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

(*
pub fn calc_linear_cost_u32(len: usize, base: u64, word: u64) -> u64 {
    (len as u64 + 32 - 1) / 32 * word + base
}
*)
Definition calc_linear_cost_u32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ len; base; word ] =>
    ltac:(M.monadic
      (let len := M.alloc (| len |) in
      let base := M.alloc (| base |) in
      let word := M.alloc (| word |) in
      BinOp.Wrap.add (|
        BinOp.Wrap.mul (|
          BinOp.Wrap.div (|
            BinOp.Wrap.sub (|
              BinOp.Wrap.add (| M.rust_cast (M.read (| len |)), Value.Integer IntegerKind.U64 32 |),
              Value.Integer IntegerKind.U64 1
            |),
            Value.Integer IntegerKind.U64 32
          |),
          M.read (| word |)
        |),
        M.read (| base |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_calc_linear_cost_u32 :
  M.IsFunction "revm_precompile::calc_linear_cost_u32" calc_linear_cost_u32.

(* StructRecord
  {
    name := "PrecompileOutput";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("cost", Ty.path "u64");
        ("output",
          Ty.apply (Ty.path "alloc::vec::Vec") [] [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]);
        ("logs",
          Ty.apply
            (Ty.path "alloc::vec::Vec")
            []
            [
              Ty.apply
                (Ty.path "alloy_primitives::log::Log")
                []
                [ Ty.path "alloy_primitives::log::LogData" ];
              Ty.path "alloc::alloc::Global"
            ])
      ];
  } *)

Module Impl_core_clone_Clone_for_revm_precompile_PrecompileOutput.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileOutput".
  
  (* 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_precompile::PrecompileOutput"
          [
            ("cost",
              M.call_closure (|
                M.get_trait_method (| "core::clone::Clone", Ty.path "u64", [], "clone", [] |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_precompile::PrecompileOutput",
                    "cost"
                  |)
                ]
              |));
            ("output",
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_precompile::PrecompileOutput",
                    "output"
                  |)
                ]
              |));
            ("logs",
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloy_primitives::log::Log")
                        []
                        [ Ty.path "alloy_primitives::log::LogData" ];
                      Ty.path "alloc::alloc::Global"
                    ],
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_precompile::PrecompileOutput",
                    "logs"
                  |)
                ]
              |))
          ]))
    | _, _, _ => 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_precompile_PrecompileOutput.

Module Impl_core_fmt_Debug_for_revm_precompile_PrecompileOutput.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileOutput".
  
  (* 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 "PrecompileOutput" |);
            M.read (| Value.String "cost" |);
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_precompile::PrecompileOutput",
              "cost"
            |);
            M.read (| Value.String "output" |);
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_precompile::PrecompileOutput",
              "output"
            |);
            M.read (| Value.String "logs" |);
            M.alloc (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_precompile::PrecompileOutput",
                "logs"
              |)
            |)
          ]
        |)))
    | _, _, _ => 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_precompile_PrecompileOutput.

Module Impl_core_default_Default_for_revm_precompile_PrecompileOutput.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileOutput".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "revm_precompile::PrecompileOutput"
          [
            ("cost",
              M.call_closure (|
                M.get_trait_method (| "core::default::Default", Ty.path "u64", [], "default", [] |),
                []
              |));
            ("output",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                  [],
                  "default",
                  []
                |),
                []
              |));
            ("logs",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloy_primitives::log::Log")
                        []
                        [ Ty.path "alloy_primitives::log::LogData" ];
                      Ty.path "alloc::alloc::Global"
                    ],
                  [],
                  "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_precompile_PrecompileOutput.

Module Impl_core_marker_StructuralPartialEq_for_revm_precompile_PrecompileOutput.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileOutput".
  
  Axiom Implements :
    M.IsTraitInstance
      "core::marker::StructuralPartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_StructuralPartialEq_for_revm_precompile_PrecompileOutput.

Module Impl_core_cmp_PartialEq_for_revm_precompile_PrecompileOutput.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileOutput".
  
  (* 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 (|
            BinOp.eq (|
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_precompile::PrecompileOutput",
                  "cost"
                |)
              |),
              M.read (|
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "revm_precompile::PrecompileOutput",
                  "cost"
                |)
              |)
            |),
            ltac:(M.monadic
              (M.call_closure (|
                M.get_trait_method (|
                  "core::cmp::PartialEq",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                  [
                    Ty.apply
                      (Ty.path "alloc::vec::Vec")
                      []
                      [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ]
                  ],
                  "eq",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_precompile::PrecompileOutput",
                    "output"
                  |);
                  M.SubPointer.get_struct_record_field (|
                    M.read (| other |),
                    "revm_precompile::PrecompileOutput",
                    "output"
                  |)
                ]
              |)))
          |),
          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::log::Log")
                      []
                      [ Ty.path "alloy_primitives::log::LogData" ];
                    Ty.path "alloc::alloc::Global"
                  ],
                [
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloy_primitives::log::Log")
                        []
                        [ Ty.path "alloy_primitives::log::LogData" ];
                      Ty.path "alloc::alloc::Global"
                    ]
                ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_precompile::PrecompileOutput",
                  "logs"
                |);
                M.SubPointer.get_struct_record_field (|
                  M.read (| other |),
                  "revm_precompile::PrecompileOutput",
                  "logs"
                |)
              ]
            |)))
        |)))
    | _, _, _ => 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_precompile_PrecompileOutput.

Module Impl_core_cmp_Eq_for_revm_precompile_PrecompileOutput.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileOutput".
  
  (* 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_precompile_PrecompileOutput.

Module Impl_core_hash_Hash_for_revm_precompile_PrecompileOutput.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileOutput".
  
  (* 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_precompile::PrecompileOutput",
                    "cost"
                  |);
                  M.read (| state |)
                ]
              |)
            |) in
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::hash::Hash",
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                  [],
                  "hash",
                  [ __H ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_precompile::PrecompileOutput",
                    "output"
                  |);
                  M.read (| state |)
                ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::hash::Hash",
                Ty.apply
                  (Ty.path "alloc::vec::Vec")
                  []
                  [
                    Ty.apply
                      (Ty.path "alloy_primitives::log::Log")
                      []
                      [ Ty.path "alloy_primitives::log::LogData" ];
                    Ty.path "alloc::alloc::Global"
                  ],
                [],
                "hash",
                [ __H ]
              |),
              [
                M.SubPointer.get_struct_record_field (|
                  M.read (| self |),
                  "revm_precompile::PrecompileOutput",
                  "logs"
                |);
                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_precompile_PrecompileOutput.

Module Impl_revm_precompile_PrecompileOutput.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileOutput".
  
  (*
      pub fn without_logs(cost: u64, output: Vec<u8>) -> Self {
          Self {
              cost,
              output,
              logs: Vec::new(),
          }
      }
  *)
  Definition without_logs (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ cost; output ] =>
      ltac:(M.monadic
        (let cost := M.alloc (| cost |) in
        let output := M.alloc (| output |) in
        Value.StructRecord
          "revm_precompile::PrecompileOutput"
          [
            ("cost", M.read (| cost |));
            ("output", M.read (| output |));
            ("logs",
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloc::vec::Vec")
                    []
                    [
                      Ty.apply
                        (Ty.path "alloy_primitives::log::Log")
                        []
                        [ Ty.path "alloy_primitives::log::LogData" ];
                      Ty.path "alloc::alloc::Global"
                    ],
                  "new",
                  []
                |),
                []
              |))
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_without_logs : M.IsAssociatedFunction Self "without_logs" without_logs.
End Impl_revm_precompile_PrecompileOutput.

(* StructRecord
  {
    name := "Precompiles";
    const_params := [];
    ty_params := [];
    fields :=
      [
        ("inner",
          Ty.apply
            (Ty.path "std::collections::hash::map::HashMap")
            []
            [
              Ty.path "alloy_primitives::bits::address::Address";
              Ty.path "revm_primitives::precompile::Precompile";
              Ty.path "std::hash::random::RandomState"
            ])
      ];
  } *)

Module Impl_core_clone_Clone_for_revm_precompile_Precompiles.
  Definition Self : Ty.t := Ty.path "revm_precompile::Precompiles".
  
  (* 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_precompile::Precompiles"
          [
            ("inner",
              M.call_closure (|
                M.get_trait_method (|
                  "core::clone::Clone",
                  Ty.apply
                    (Ty.path "std::collections::hash::map::HashMap")
                    []
                    [
                      Ty.path "alloy_primitives::bits::address::Address";
                      Ty.path "revm_primitives::precompile::Precompile";
                      Ty.path "std::hash::random::RandomState"
                    ],
                  [],
                  "clone",
                  []
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_precompile::Precompiles",
                    "inner"
                  |)
                ]
              |))
          ]))
    | _, _, _ => 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_precompile_Precompiles.

Module Impl_core_default_Default_for_revm_precompile_Precompiles.
  Definition Self : Ty.t := Ty.path "revm_precompile::Precompiles".
  
  (* Default *)
  Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (Value.StructRecord
          "revm_precompile::Precompiles"
          [
            ("inner",
              M.call_closure (|
                M.get_trait_method (|
                  "core::default::Default",
                  Ty.apply
                    (Ty.path "std::collections::hash::map::HashMap")
                    []
                    [
                      Ty.path "alloy_primitives::bits::address::Address";
                      Ty.path "revm_primitives::precompile::Precompile";
                      Ty.path "std::hash::random::RandomState"
                    ],
                  [],
                  "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_precompile_Precompiles.

Module Impl_core_fmt_Debug_for_revm_precompile_Precompiles.
  Definition Self : Ty.t := Ty.path "revm_precompile::Precompiles".
  
  (* Debug *)
  Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.path "core::fmt::Formatter",
            "debug_struct_field1_finish",
            []
          |),
          [
            M.read (| f |);
            M.read (| Value.String "Precompiles" |);
            M.read (| Value.String "inner" |);
            M.alloc (|
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_precompile::Precompiles",
                "inner"
              |)
            |)
          ]
        |)))
    | _, _, _ => 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_precompile_Precompiles.

Module Impl_revm_precompile_Precompiles.
  Definition Self : Ty.t := Ty.path "revm_precompile::Precompiles".
  
  (*
      pub fn new(spec: PrecompileSpecId) -> &'static Self {
          match spec {
              PrecompileSpecId::HOMESTEAD => Self::homestead(),
              PrecompileSpecId::BYZANTIUM => Self::byzantium(),
              PrecompileSpecId::ISTANBUL => Self::istanbul(),
              PrecompileSpecId::BERLIN => Self::berlin(),
              PrecompileSpecId::CANCUN => Self::cancun(),
              PrecompileSpecId::LATEST => Self::latest(),
          }
      }
  *)
  Definition new (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ spec ] =>
      ltac:(M.monadic
        (let spec := M.alloc (| spec |) in
        M.read (|
          M.match_operator (|
            spec,
            [
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_struct_tuple (| γ, "revm_precompile::PrecompileSpecId::HOMESTEAD" |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_precompile::Precompiles",
                        "homestead",
                        []
                      |),
                      []
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_struct_tuple (| γ, "revm_precompile::PrecompileSpecId::BYZANTIUM" |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_precompile::Precompiles",
                        "byzantium",
                        []
                      |),
                      []
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_struct_tuple (| γ, "revm_precompile::PrecompileSpecId::ISTANBUL" |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_precompile::Precompiles",
                        "istanbul",
                        []
                      |),
                      []
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_struct_tuple (| γ, "revm_precompile::PrecompileSpecId::BERLIN" |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_precompile::Precompiles",
                        "berlin",
                        []
                      |),
                      []
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_struct_tuple (| γ, "revm_precompile::PrecompileSpecId::CANCUN" |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_precompile::Precompiles",
                        "cancun",
                        []
                      |),
                      []
                    |)
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_struct_tuple (| γ, "revm_precompile::PrecompileSpecId::LATEST" |) in
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (|
                        Ty.path "revm_precompile::Precompiles",
                        "latest",
                        []
                      |),
                      []
                    |)
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_new : M.IsAssociatedFunction Self "new" new.
  
  (*
      pub fn homestead() -> &'static Self {
          static INSTANCE: OnceBox<Precompiles> = OnceBox::new();
          INSTANCE.get_or_init(|| {
              let mut precompiles = Precompiles::default();
              precompiles.extend([
                  secp256k1::ECRECOVER,
                  hash::SHA256,
                  hash::RIPEMD160,
                  identity::FUN,
              ]);
              Box::new(precompiles)
          })
      }
  *)
  Definition homestead (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "once_cell::race::once_box::OnceBox")
              []
              [ Ty.path "revm_precompile::Precompiles" ],
            "get_or_init",
            [
              Ty.function
                [ Ty.tuple [] ]
                (Ty.apply
                  (Ty.path "alloc::boxed::Box")
                  []
                  [ Ty.path "revm_precompile::Precompiles"; Ty.path "alloc::alloc::Global" ])
            ]
          |),
          [
            M.read (| M.get_constant (| "revm_precompile::homestead::INSTANCE" |) |);
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (M.read (|
                                let~ precompiles :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::default::Default",
                                        Ty.path "revm_precompile::Precompiles",
                                        [],
                                        "default",
                                        []
                                      |),
                                      []
                                    |)
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_precompile::Precompiles",
                                        "extend",
                                        [
                                          Ty.apply
                                            (Ty.path "array")
                                            [ Value.Integer IntegerKind.Usize 4 ]
                                            [ Ty.path "revm_precompile::PrecompileWithAddress" ]
                                        ]
                                      |),
                                      [
                                        precompiles;
                                        Value.Array
                                          [
                                            M.read (|
                                              M.get_constant (|
                                                "revm_precompile::secp256k1::ECRECOVER"
                                              |)
                                            |);
                                            M.read (|
                                              M.get_constant (| "revm_precompile::hash::SHA256" |)
                                            |);
                                            M.read (|
                                              M.get_constant (|
                                                "revm_precompile::hash::RIPEMD160"
                                              |)
                                            |);
                                            M.read (|
                                              M.get_constant (| "revm_precompile::identity::FUN" |)
                                            |)
                                          ]
                                      ]
                                    |)
                                  |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::boxed::Box")
                                        []
                                        [
                                          Ty.path "revm_precompile::Precompiles";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "new",
                                      []
                                    |),
                                    [ M.read (| precompiles |) ]
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_homestead : M.IsAssociatedFunction Self "homestead" homestead.
  
  (*
      pub fn byzantium() -> &'static Self {
          static INSTANCE: OnceBox<Precompiles> = OnceBox::new();
          INSTANCE.get_or_init(|| {
              let mut precompiles = Self::homestead().clone();
              precompiles.extend([
                  // EIP-196: Precompiled contracts for addition and scalar multiplication on the elliptic curve alt_bn128.
                  // EIP-197: Precompiled contracts for optimal ate pairing check on the elliptic curve alt_bn128.
                  bn128::add::BYZANTIUM,
                  bn128::mul::BYZANTIUM,
                  bn128::pair::BYZANTIUM,
                  // EIP-198: Big integer modular exponentiation.
                  modexp::BYZANTIUM,
              ]);
              Box::new(precompiles)
          })
      }
  *)
  Definition byzantium (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "once_cell::race::once_box::OnceBox")
              []
              [ Ty.path "revm_precompile::Precompiles" ],
            "get_or_init",
            [
              Ty.function
                [ Ty.tuple [] ]
                (Ty.apply
                  (Ty.path "alloc::boxed::Box")
                  []
                  [ Ty.path "revm_precompile::Precompiles"; Ty.path "alloc::alloc::Global" ])
            ]
          |),
          [
            M.read (| M.get_constant (| "revm_precompile::byzantium::INSTANCE" |) |);
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (M.read (|
                                let~ precompiles :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::clone::Clone",
                                        Ty.path "revm_precompile::Precompiles",
                                        [],
                                        "clone",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_precompile::Precompiles",
                                            "homestead",
                                            []
                                          |),
                                          []
                                        |)
                                      ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_precompile::Precompiles",
                                        "extend",
                                        [
                                          Ty.apply
                                            (Ty.path "array")
                                            [ Value.Integer IntegerKind.Usize 4 ]
                                            [ Ty.path "revm_precompile::PrecompileWithAddress" ]
                                        ]
                                      |),
                                      [
                                        precompiles;
                                        Value.Array
                                          [
                                            M.read (|
                                              M.get_constant (|
                                                "revm_precompile::bn128::add::BYZANTIUM"
                                              |)
                                            |);
                                            M.read (|
                                              M.get_constant (|
                                                "revm_precompile::bn128::mul::BYZANTIUM"
                                              |)
                                            |);
                                            M.read (|
                                              M.get_constant (|
                                                "revm_precompile::bn128::pair::BYZANTIUM"
                                              |)
                                            |);
                                            M.read (|
                                              M.get_constant (|
                                                "revm_precompile::modexp::BYZANTIUM"
                                              |)
                                            |)
                                          ]
                                      ]
                                    |)
                                  |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::boxed::Box")
                                        []
                                        [
                                          Ty.path "revm_precompile::Precompiles";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "new",
                                      []
                                    |),
                                    [ M.read (| precompiles |) ]
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_byzantium : M.IsAssociatedFunction Self "byzantium" byzantium.
  
  (*
      pub fn istanbul() -> &'static Self {
          static INSTANCE: OnceBox<Precompiles> = OnceBox::new();
          INSTANCE.get_or_init(|| {
              let mut precompiles = Self::byzantium().clone();
              precompiles.extend([
                  // EIP-152: Add BLAKE2 compression function `F` precompile.
                  blake2::FUN,
                  // EIP-1108: Reduce alt_bn128 precompile gas costs.
                  bn128::add::ISTANBUL,
                  bn128::mul::ISTANBUL,
                  bn128::pair::ISTANBUL,
              ]);
              Box::new(precompiles)
          })
      }
  *)
  Definition istanbul (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "once_cell::race::once_box::OnceBox")
              []
              [ Ty.path "revm_precompile::Precompiles" ],
            "get_or_init",
            [
              Ty.function
                [ Ty.tuple [] ]
                (Ty.apply
                  (Ty.path "alloc::boxed::Box")
                  []
                  [ Ty.path "revm_precompile::Precompiles"; Ty.path "alloc::alloc::Global" ])
            ]
          |),
          [
            M.read (| M.get_constant (| "revm_precompile::istanbul::INSTANCE" |) |);
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (M.read (|
                                let~ precompiles :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::clone::Clone",
                                        Ty.path "revm_precompile::Precompiles",
                                        [],
                                        "clone",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_precompile::Precompiles",
                                            "byzantium",
                                            []
                                          |),
                                          []
                                        |)
                                      ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_precompile::Precompiles",
                                        "extend",
                                        [
                                          Ty.apply
                                            (Ty.path "array")
                                            [ Value.Integer IntegerKind.Usize 4 ]
                                            [ Ty.path "revm_precompile::PrecompileWithAddress" ]
                                        ]
                                      |),
                                      [
                                        precompiles;
                                        Value.Array
                                          [
                                            M.read (|
                                              M.get_constant (| "revm_precompile::blake2::FUN" |)
                                            |);
                                            M.read (|
                                              M.get_constant (|
                                                "revm_precompile::bn128::add::ISTANBUL"
                                              |)
                                            |);
                                            M.read (|
                                              M.get_constant (|
                                                "revm_precompile::bn128::mul::ISTANBUL"
                                              |)
                                            |);
                                            M.read (|
                                              M.get_constant (|
                                                "revm_precompile::bn128::pair::ISTANBUL"
                                              |)
                                            |)
                                          ]
                                      ]
                                    |)
                                  |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::boxed::Box")
                                        []
                                        [
                                          Ty.path "revm_precompile::Precompiles";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "new",
                                      []
                                    |),
                                    [ M.read (| precompiles |) ]
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_istanbul : M.IsAssociatedFunction Self "istanbul" istanbul.
  
  (*
      pub fn berlin() -> &'static Self {
          static INSTANCE: OnceBox<Precompiles> = OnceBox::new();
          INSTANCE.get_or_init(|| {
              let mut precompiles = Self::istanbul().clone();
              precompiles.extend([
                  // EIP-2565: ModExp Gas Cost.
                  modexp::BERLIN,
              ]);
              Box::new(precompiles)
          })
      }
  *)
  Definition berlin (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "once_cell::race::once_box::OnceBox")
              []
              [ Ty.path "revm_precompile::Precompiles" ],
            "get_or_init",
            [
              Ty.function
                [ Ty.tuple [] ]
                (Ty.apply
                  (Ty.path "alloc::boxed::Box")
                  []
                  [ Ty.path "revm_precompile::Precompiles"; Ty.path "alloc::alloc::Global" ])
            ]
          |),
          [
            M.read (| M.get_constant (| "revm_precompile::berlin::INSTANCE" |) |);
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (M.read (|
                                let~ precompiles :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::clone::Clone",
                                        Ty.path "revm_precompile::Precompiles",
                                        [],
                                        "clone",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_precompile::Precompiles",
                                            "istanbul",
                                            []
                                          |),
                                          []
                                        |)
                                      ]
                                    |)
                                  |) in
                                let~ _ :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path "revm_precompile::Precompiles",
                                        "extend",
                                        [
                                          Ty.apply
                                            (Ty.path "array")
                                            [ Value.Integer IntegerKind.Usize 1 ]
                                            [ Ty.path "revm_precompile::PrecompileWithAddress" ]
                                        ]
                                      |),
                                      [
                                        precompiles;
                                        Value.Array
                                          [
                                            M.read (|
                                              M.get_constant (| "revm_precompile::modexp::BERLIN" |)
                                            |)
                                          ]
                                      ]
                                    |)
                                  |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::boxed::Box")
                                        []
                                        [
                                          Ty.path "revm_precompile::Precompiles";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "new",
                                      []
                                    |),
                                    [ M.read (| precompiles |) ]
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_berlin : M.IsAssociatedFunction Self "berlin" berlin.
  
  (*
      pub fn cancun() -> &'static Self {
          static INSTANCE: OnceBox<Precompiles> = OnceBox::new();
          INSTANCE.get_or_init(|| {
              let precompiles = Self::berlin().clone();
  
              // Don't include KZG point evaluation precompile in no_std builds.
              #[cfg(feature = "c-kzg")]
              let precompiles = {
                  let mut precompiles = precompiles;
                  precompiles.extend([
                      // EIP-4844: Shard Blob Transactions
                      kzg_point_evaluation::POINT_EVALUATION,
                  ]);
                  precompiles
              };
  
              Box::new(precompiles)
          })
      }
  *)
  Definition cancun (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "once_cell::race::once_box::OnceBox")
              []
              [ Ty.path "revm_precompile::Precompiles" ],
            "get_or_init",
            [
              Ty.function
                [ Ty.tuple [] ]
                (Ty.apply
                  (Ty.path "alloc::boxed::Box")
                  []
                  [ Ty.path "revm_precompile::Precompiles"; Ty.path "alloc::alloc::Global" ])
            ]
          |),
          [
            M.read (| M.get_constant (| "revm_precompile::cancun::INSTANCE" |) |);
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (M.read (|
                                let~ precompiles :=
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::clone::Clone",
                                        Ty.path "revm_precompile::Precompiles",
                                        [],
                                        "clone",
                                        []
                                      |),
                                      [
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_precompile::Precompiles",
                                            "berlin",
                                            []
                                          |),
                                          []
                                        |)
                                      ]
                                    |)
                                  |) in
                                let~ precompiles :=
                                  M.copy (|
                                    let~ precompiles := M.copy (| precompiles |) in
                                    let~ _ :=
                                      M.alloc (|
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "revm_precompile::Precompiles",
                                            "extend",
                                            [
                                              Ty.apply
                                                (Ty.path "array")
                                                [ Value.Integer IntegerKind.Usize 1 ]
                                                [ Ty.path "revm_precompile::PrecompileWithAddress" ]
                                            ]
                                          |),
                                          [
                                            precompiles;
                                            Value.Array
                                              [
                                                M.read (|
                                                  M.get_constant (|
                                                    "revm_precompile::kzg_point_evaluation::POINT_EVALUATION"
                                                  |)
                                                |)
                                              ]
                                          ]
                                        |)
                                      |) in
                                    precompiles
                                  |) in
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "alloc::boxed::Box")
                                        []
                                        [
                                          Ty.path "revm_precompile::Precompiles";
                                          Ty.path "alloc::alloc::Global"
                                        ],
                                      "new",
                                      []
                                    |),
                                    [ M.read (| precompiles |) ]
                                  |)
                                |)
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_cancun : M.IsAssociatedFunction Self "cancun" cancun.
  
  (*
      pub fn latest() -> &'static Self {
          Self::cancun()
      }
  *)
  Definition latest (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [] =>
      ltac:(M.monadic
        (M.call_closure (|
          M.get_associated_function (| Ty.path "revm_precompile::Precompiles", "cancun", [] |),
          []
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_latest : M.IsAssociatedFunction Self "latest" latest.
  
  (*
      pub fn addresses(&self) -> impl Iterator<Item = &Address> {
          self.inner.keys()
      }
  *)
  Definition addresses (ε : 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 "std::collections::hash::map::HashMap")
              []
              [
                Ty.path "alloy_primitives::bits::address::Address";
                Ty.path "revm_primitives::precompile::Precompile";
                Ty.path "std::hash::random::RandomState"
              ],
            "keys",
            []
          |),
          [
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_precompile::Precompiles",
              "inner"
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_addresses : M.IsAssociatedFunction Self "addresses" addresses.
  
  (*
      pub fn into_addresses(self) -> impl Iterator<Item = Address> {
          self.inner.into_keys()
      }
  *)
  Definition into_addresses (ε : 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 "std::collections::hash::map::HashMap")
              []
              [
                Ty.path "alloy_primitives::bits::address::Address";
                Ty.path "revm_primitives::precompile::Precompile";
                Ty.path "std::hash::random::RandomState"
              ],
            "into_keys",
            []
          |),
          [
            M.read (|
              M.SubPointer.get_struct_record_field (|
                self,
                "revm_precompile::Precompiles",
                "inner"
              |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_into_addresses :
    M.IsAssociatedFunction Self "into_addresses" into_addresses.
  
  (*
      pub fn contains(&self, address: &Address) -> bool {
          self.inner.contains_key(address)
      }
  *)
  Definition contains (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; address ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let address := M.alloc (| address |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "std::collections::hash::map::HashMap")
              []
              [
                Ty.path "alloy_primitives::bits::address::Address";
                Ty.path "revm_primitives::precompile::Precompile";
                Ty.path "std::hash::random::RandomState"
              ],
            "contains_key",
            [ Ty.path "alloy_primitives::bits::address::Address" ]
          |),
          [
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_precompile::Precompiles",
              "inner"
            |);
            M.read (| address |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_contains : M.IsAssociatedFunction Self "contains" contains.
  
  (*
      pub fn get(&self, address: &Address) -> Option<&Precompile> {
          self.inner.get(address)
      }
  *)
  Definition get (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; address ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let address := M.alloc (| address |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "std::collections::hash::map::HashMap")
              []
              [
                Ty.path "alloy_primitives::bits::address::Address";
                Ty.path "revm_primitives::precompile::Precompile";
                Ty.path "std::hash::random::RandomState"
              ],
            "get",
            [ Ty.path "alloy_primitives::bits::address::Address" ]
          |),
          [
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_precompile::Precompiles",
              "inner"
            |);
            M.read (| address |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get : M.IsAssociatedFunction Self "get" get.
  
  (*
      pub fn get_mut(&mut self, address: &Address) -> Option<&mut Precompile> {
          self.inner.get_mut(address)
      }
  *)
  Definition get_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; address ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let address := M.alloc (| address |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "std::collections::hash::map::HashMap")
              []
              [
                Ty.path "alloy_primitives::bits::address::Address";
                Ty.path "revm_primitives::precompile::Precompile";
                Ty.path "std::hash::random::RandomState"
              ],
            "get_mut",
            [ Ty.path "alloy_primitives::bits::address::Address" ]
          |),
          [
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_precompile::Precompiles",
              "inner"
            |);
            M.read (| address |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_get_mut : M.IsAssociatedFunction Self "get_mut" get_mut.
  
  (*
      pub fn is_empty(&self) -> bool {
          self.inner.len() == 0
      }
  *)
  Definition is_empty (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        BinOp.eq (|
          M.call_closure (|
            M.get_associated_function (|
              Ty.apply
                (Ty.path "std::collections::hash::map::HashMap")
                []
                [
                  Ty.path "alloy_primitives::bits::address::Address";
                  Ty.path "revm_primitives::precompile::Precompile";
                  Ty.path "std::hash::random::RandomState"
                ],
              "len",
              []
            |),
            [
              M.SubPointer.get_struct_record_field (|
                M.read (| self |),
                "revm_precompile::Precompiles",
                "inner"
              |)
            ]
          |),
          Value.Integer IntegerKind.Usize 0
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_is_empty : M.IsAssociatedFunction Self "is_empty" is_empty.
  
  (*
      pub fn len(&self) -> usize {
          self.inner.len()
      }
  *)
  Definition len (ε : 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 "std::collections::hash::map::HashMap")
              []
              [
                Ty.path "alloy_primitives::bits::address::Address";
                Ty.path "revm_primitives::precompile::Precompile";
                Ty.path "std::hash::random::RandomState"
              ],
            "len",
            []
          |),
          [
            M.SubPointer.get_struct_record_field (|
              M.read (| self |),
              "revm_precompile::Precompiles",
              "inner"
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_len : M.IsAssociatedFunction Self "len" len.
  
  (*
      pub fn extend(&mut self, other: impl IntoIterator<Item = PrecompileWithAddress>) {
          self.inner.extend(other.into_iter().map(Into::into));
      }
  *)
  Definition extend (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ impl_IntoIterator_Item___PrecompileWithAddress_ ], [ self; other ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        M.read (|
          let~ _ :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::iter::traits::collect::Extend",
                  Ty.apply
                    (Ty.path "std::collections::hash::map::HashMap")
                    []
                    [
                      Ty.path "alloy_primitives::bits::address::Address";
                      Ty.path "revm_primitives::precompile::Precompile";
                      Ty.path "std::hash::random::RandomState"
                    ],
                  [
                    Ty.tuple
                      [
                        Ty.path "alloy_primitives::bits::address::Address";
                        Ty.path "revm_primitives::precompile::Precompile"
                      ]
                  ],
                  "extend",
                  [
                    Ty.apply
                      (Ty.path "core::iter::adapters::map::Map")
                      []
                      [
                        Ty.associated;
                        Ty.function
                          [ Ty.path "revm_precompile::PrecompileWithAddress" ]
                          (Ty.tuple
                            [
                              Ty.path "alloy_primitives::bits::address::Address";
                              Ty.path "revm_primitives::precompile::Precompile"
                            ])
                      ]
                  ]
                |),
                [
                  M.SubPointer.get_struct_record_field (|
                    M.read (| self |),
                    "revm_precompile::Precompiles",
                    "inner"
                  |);
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::iter::traits::iterator::Iterator",
                      Ty.associated,
                      [],
                      "map",
                      [
                        Ty.tuple
                          [
                            Ty.path "alloy_primitives::bits::address::Address";
                            Ty.path "revm_primitives::precompile::Precompile"
                          ];
                        Ty.function
                          [ Ty.path "revm_precompile::PrecompileWithAddress" ]
                          (Ty.tuple
                            [
                              Ty.path "alloy_primitives::bits::address::Address";
                              Ty.path "revm_primitives::precompile::Precompile"
                            ])
                      ]
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::iter::traits::collect::IntoIterator",
                          impl_IntoIterator_Item___PrecompileWithAddress_,
                          [],
                          "into_iter",
                          []
                        |),
                        [ M.read (| other |) ]
                      |);
                      M.get_trait_method (|
                        "core::convert::Into",
                        Ty.path "revm_precompile::PrecompileWithAddress",
                        [
                          Ty.tuple
                            [
                              Ty.path "alloy_primitives::bits::address::Address";
                              Ty.path "revm_primitives::precompile::Precompile"
                            ]
                        ],
                        "into",
                        []
                      |)
                    ]
                  |)
                ]
              |)
            |) in
          M.alloc (| Value.Tuple [] |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_extend : M.IsAssociatedFunction Self "extend" extend.
End Impl_revm_precompile_Precompiles.

(* StructTuple
  {
    name := "PrecompileWithAddress";
    const_params := [];
    ty_params := [];
    fields :=
      [
        Ty.path "alloy_primitives::bits::address::Address";
        Ty.path "revm_primitives::precompile::Precompile"
      ];
  } *)

Module Impl_core_clone_Clone_for_revm_precompile_PrecompileWithAddress.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileWithAddress".
  
  (* 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.StructTuple
          "revm_precompile::PrecompileWithAddress"
          [
            M.call_closure (|
              M.get_trait_method (|
                "core::clone::Clone",
                Ty.path "alloy_primitives::bits::address::Address",
                [],
                "clone",
                []
              |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "revm_precompile::PrecompileWithAddress",
                  0
                |)
              ]
            |);
            M.call_closure (|
              M.get_trait_method (|
                "core::clone::Clone",
                Ty.path "revm_primitives::precompile::Precompile",
                [],
                "clone",
                []
              |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "revm_precompile::PrecompileWithAddress",
                  1
                |)
              ]
            |)
          ]))
    | _, _, _ => 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_precompile_PrecompileWithAddress.

Module Impl_core_fmt_Debug_for_revm_precompile_PrecompileWithAddress.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileWithAddress".
  
  (* Debug *)
  Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; f ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let f := M.alloc (| f |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.path "core::fmt::Formatter",
            "debug_tuple_field2_finish",
            []
          |),
          [
            M.read (| f |);
            M.read (| Value.String "PrecompileWithAddress" |);
            M.SubPointer.get_struct_tuple_field (|
              M.read (| self |),
              "revm_precompile::PrecompileWithAddress",
              0
            |);
            M.alloc (|
              M.SubPointer.get_struct_tuple_field (|
                M.read (| self |),
                "revm_precompile::PrecompileWithAddress",
                1
              |)
            |)
          ]
        |)))
    | _, _, _ => 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_precompile_PrecompileWithAddress.

Module Impl_core_convert_From_Tuple_alloy_primitives_bits_address_Address_revm_primitives_precompile_Precompile__for_revm_precompile_PrecompileWithAddress.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileWithAddress".
  
  (*
      fn from(value: (Address, Precompile)) -> Self {
          PrecompileWithAddress(value.0, value.1)
      }
  *)
  Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ value ] =>
      ltac:(M.monadic
        (let value := M.alloc (| value |) in
        Value.StructTuple
          "revm_precompile::PrecompileWithAddress"
          [
            M.read (| M.SubPointer.get_tuple_field (| value, 0 |) |);
            M.read (| M.SubPointer.get_tuple_field (| value, 1 |) |)
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::convert::From"
      Self
      (* Trait polymorphic types *)
      [
        (* T *)
        Ty.tuple
          [
            Ty.path "alloy_primitives::bits::address::Address";
            Ty.path "revm_primitives::precompile::Precompile"
          ]
      ]
      (* Instance *) [ ("from", InstanceField.Method from) ].
End Impl_core_convert_From_Tuple_alloy_primitives_bits_address_Address_revm_primitives_precompile_Precompile__for_revm_precompile_PrecompileWithAddress.

Module Impl_core_convert_From_revm_precompile_PrecompileWithAddress_for_Tuple_alloy_primitives_bits_address_Address_revm_primitives_precompile_Precompile_.
  Definition Self : Ty.t :=
    Ty.tuple
      [
        Ty.path "alloy_primitives::bits::address::Address";
        Ty.path "revm_primitives::precompile::Precompile"
      ].
  
  (*
      fn from(value: PrecompileWithAddress) -> Self {
          (value.0, value.1)
      }
  *)
  Definition from (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ value ] =>
      ltac:(M.monadic
        (let value := M.alloc (| value |) in
        Value.Tuple
          [
            M.read (|
              M.SubPointer.get_struct_tuple_field (|
                value,
                "revm_precompile::PrecompileWithAddress",
                0
              |)
            |);
            M.read (|
              M.SubPointer.get_struct_tuple_field (|
                value,
                "revm_precompile::PrecompileWithAddress",
                1
              |)
            |)
          ]))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::convert::From"
      Self
      (* Trait polymorphic types *) [ (* T *) Ty.path "revm_precompile::PrecompileWithAddress" ]
      (* Instance *) [ ("from", InstanceField.Method from) ].
End Impl_core_convert_From_revm_precompile_PrecompileWithAddress_for_Tuple_alloy_primitives_bits_address_Address_revm_primitives_precompile_Precompile_.

(*
Enum PrecompileSpecId
{
  const_params := [];
  ty_params := [];
  variants :=
    [
      {
        name := "HOMESTEAD";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "BYZANTIUM";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "ISTANBUL";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "BERLIN";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "CANCUN";
        item := StructTuple [];
        discriminant := None;
      };
      {
        name := "LATEST";
        item := StructTuple [];
        discriminant := None;
      }
    ];
}
*)

Module Impl_core_marker_Copy_for_revm_precompile_PrecompileSpecId.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileSpecId".
  
  Axiom Implements :
    M.IsTraitInstance "core::marker::Copy" Self (* Trait polymorphic types *) [] (* Instance *) [].
End Impl_core_marker_Copy_for_revm_precompile_PrecompileSpecId.

Module Impl_core_clone_Clone_for_revm_precompile_PrecompileSpecId.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileSpecId".
  
  (* 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.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_precompile_PrecompileSpecId.

Module Impl_core_fmt_Debug_for_revm_precompile_PrecompileSpecId.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileSpecId".
  
  (* 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_precompile::PrecompileSpecId::HOMESTEAD" |) in
                      M.alloc (| M.read (| Value.String "HOMESTEAD" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "revm_precompile::PrecompileSpecId::BYZANTIUM" |) in
                      M.alloc (| M.read (| Value.String "BYZANTIUM" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "revm_precompile::PrecompileSpecId::ISTANBUL" |) in
                      M.alloc (| M.read (| Value.String "ISTANBUL" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "revm_precompile::PrecompileSpecId::BERLIN" |) in
                      M.alloc (| M.read (| Value.String "BERLIN" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "revm_precompile::PrecompileSpecId::CANCUN" |) in
                      M.alloc (| M.read (| Value.String "CANCUN" |) |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (| γ, "revm_precompile::PrecompileSpecId::LATEST" |) in
                      M.alloc (| M.read (| Value.String "LATEST" |) |)))
                ]
              |)
            |)
          ]
        |)))
    | _, _, _ => 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_precompile_PrecompileSpecId.

Module Impl_core_marker_StructuralPartialEq_for_revm_precompile_PrecompileSpecId.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileSpecId".
  
  Axiom Implements :
    M.IsTraitInstance
      "core::marker::StructuralPartialEq"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [].
End Impl_core_marker_StructuralPartialEq_for_revm_precompile_PrecompileSpecId.

Module Impl_core_cmp_PartialEq_for_revm_precompile_PrecompileSpecId.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileSpecId".
  
  (* 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_precompile::PrecompileSpecId" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "revm_precompile::PrecompileSpecId" ]
                |),
                [ 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_precompile_PrecompileSpecId.

Module Impl_core_cmp_Eq_for_revm_precompile_PrecompileSpecId.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileSpecId".
  
  (* 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_precompile_PrecompileSpecId.

Module Impl_core_hash_Hash_for_revm_precompile_PrecompileSpecId.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileSpecId".
  
  (* 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_precompile::PrecompileSpecId" ]
                |),
                [ 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_precompile_PrecompileSpecId.

Module Impl_core_cmp_Ord_for_revm_precompile_PrecompileSpecId.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileSpecId".
  
  (* Ord *)
  Definition cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        M.read (|
          let~ __self_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "revm_precompile::PrecompileSpecId" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "revm_precompile::PrecompileSpecId" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (| "core::cmp::Ord", Ty.path "isize", [], "cmp", [] |),
              [ __self_discr; __arg1_discr ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::Ord"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("cmp", InstanceField.Method cmp) ].
End Impl_core_cmp_Ord_for_revm_precompile_PrecompileSpecId.

Module Impl_core_cmp_PartialOrd_for_revm_precompile_PrecompileSpecId.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileSpecId".
  
  (* PartialOrd *)
  Definition partial_cmp (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ self; other ] =>
      ltac:(M.monadic
        (let self := M.alloc (| self |) in
        let other := M.alloc (| other |) in
        M.read (|
          let~ __self_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "revm_precompile::PrecompileSpecId" ]
                |),
                [ M.read (| self |) ]
              |)
            |) in
          let~ __arg1_discr :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "core::intrinsics::discriminant_value",
                  [ Ty.path "revm_precompile::PrecompileSpecId" ]
                |),
                [ M.read (| other |) ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialOrd",
                Ty.path "isize",
                [ Ty.path "isize" ],
                "partial_cmp",
                []
              |),
              [ __self_discr; __arg1_discr ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Implements :
    M.IsTraitInstance
      "core::cmp::PartialOrd"
      Self
      (* Trait polymorphic types *) []
      (* Instance *) [ ("partial_cmp", InstanceField.Method partial_cmp) ].
End Impl_core_cmp_PartialOrd_for_revm_precompile_PrecompileSpecId.

Module Impl_revm_precompile_PrecompileSpecId.
  Definition Self : Ty.t := Ty.path "revm_precompile::PrecompileSpecId".
  
  (*
      pub const fn from_spec_id(spec_id: revm_primitives::SpecId) -> Self {
          use revm_primitives::SpecId::*;
          match spec_id {
              FRONTIER | FRONTIER_THAWING | HOMESTEAD | DAO_FORK | TANGERINE | SPURIOUS_DRAGON => {
                  Self::HOMESTEAD
              }
              BYZANTIUM | CONSTANTINOPLE | PETERSBURG => Self::BYZANTIUM,
              ISTANBUL | MUIR_GLACIER => Self::ISTANBUL,
              BERLIN | LONDON | ARROW_GLACIER | GRAY_GLACIER | MERGE | SHANGHAI => Self::BERLIN,
              CANCUN | PRAGUE => Self::CANCUN,
              LATEST => Self::LATEST,
              #[cfg(feature = "optimism")]
              BEDROCK | REGOLITH | CANYON => Self::BERLIN,
              #[cfg(feature = "optimism")]
              ECOTONE => Self::CANCUN,
          }
      }
  *)
  Definition from_spec_id (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ spec_id ] =>
      ltac:(M.monadic
        (let spec_id := M.alloc (| spec_id |) in
        M.read (|
          M.match_operator (|
            spec_id,
            [
              fun γ =>
                ltac:(M.monadic
                  (M.find_or_pattern (|
                    γ,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::FRONTIER"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::FRONTIER_THAWING"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::HOMESTEAD"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::DAO_FORK"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::TANGERINE"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::SPURIOUS_DRAGON"
                            |) in
                          Value.Tuple []))
                    ],
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [] =>
                            ltac:(M.monadic
                              (M.alloc (|
                                Value.StructTuple "revm_precompile::PrecompileSpecId::HOMESTEAD" []
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (M.find_or_pattern (|
                    γ,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::BYZANTIUM"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::CONSTANTINOPLE"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::PETERSBURG"
                            |) in
                          Value.Tuple []))
                    ],
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [] =>
                            ltac:(M.monadic
                              (M.alloc (|
                                Value.StructTuple "revm_precompile::PrecompileSpecId::BYZANTIUM" []
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (M.find_or_pattern (|
                    γ,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::ISTANBUL"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::MUIR_GLACIER"
                            |) in
                          Value.Tuple []))
                    ],
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [] =>
                            ltac:(M.monadic
                              (M.alloc (|
                                Value.StructTuple "revm_precompile::PrecompileSpecId::ISTANBUL" []
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (M.find_or_pattern (|
                    γ,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::BERLIN"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::LONDON"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::ARROW_GLACIER"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::GRAY_GLACIER"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::MERGE"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::SHANGHAI"
                            |) in
                          Value.Tuple []))
                    ],
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [] =>
                            ltac:(M.monadic
                              (M.alloc (|
                                Value.StructTuple "revm_precompile::PrecompileSpecId::BERLIN" []
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (M.find_or_pattern (|
                    γ,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::CANCUN"
                            |) in
                          Value.Tuple []));
                      fun γ =>
                        ltac:(M.monadic
                          (let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::specification::SpecId::PRAGUE"
                            |) in
                          Value.Tuple []))
                    ],
                    M.closure
                      (fun γ =>
                        ltac:(M.monadic
                          match γ with
                          | [] =>
                            ltac:(M.monadic
                              (M.alloc (|
                                Value.StructTuple "revm_precompile::PrecompileSpecId::CANCUN" []
                              |)))
                          | _ => M.impossible "wrong number of arguments"
                          end))
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let _ :=
                    M.is_struct_tuple (| γ, "revm_primitives::specification::SpecId::LATEST" |) in
                  M.alloc (| Value.StructTuple "revm_precompile::PrecompileSpecId::LATEST" [] |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom AssociatedFunction_from_spec_id : M.IsAssociatedFunction Self "from_spec_id" from_spec_id.
End Impl_revm_precompile_PrecompileSpecId.

(*
pub const fn u64_to_address(x: u64) -> Address {
    let x = x.to_be_bytes();
    Address::new([
        0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, x[0], x[1], x[2], x[3], x[4], x[5], x[6], x[7],
    ])
}
*)
Definition u64_to_address (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ x ] =>
    ltac:(M.monadic
      (let x := M.alloc (| x |) in
      M.read (|
        let~ x :=
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (| Ty.path "u64", "to_be_bytes", [] |),
              [ M.read (| x |) ]
            |)
          |) in
        M.alloc (|
          M.call_closure (|
            M.get_associated_function (|
              Ty.path "alloy_primitives::bits::address::Address",
              "new",
              []
            |),
            [
              Value.Array
                [
                  Value.Integer IntegerKind.U8 0;
                  Value.Integer IntegerKind.U8 0;
                  Value.Integer IntegerKind.U8 0;
                  Value.Integer IntegerKind.U8 0;
                  Value.Integer IntegerKind.U8 0;
                  Value.Integer IntegerKind.U8 0;
                  Value.Integer IntegerKind.U8 0;
                  Value.Integer IntegerKind.U8 0;
                  Value.Integer IntegerKind.U8 0;
                  Value.Integer IntegerKind.U8 0;
                  Value.Integer IntegerKind.U8 0;
                  Value.Integer IntegerKind.U8 0;
                  M.read (|
                    M.SubPointer.get_array_field (|
                      x,
                      M.alloc (| Value.Integer IntegerKind.Usize 0 |)
                    |)
                  |);
                  M.read (|
                    M.SubPointer.get_array_field (|
                      x,
                      M.alloc (| Value.Integer IntegerKind.Usize 1 |)
                    |)
                  |);
                  M.read (|
                    M.SubPointer.get_array_field (|
                      x,
                      M.alloc (| Value.Integer IntegerKind.Usize 2 |)
                    |)
                  |);
                  M.read (|
                    M.SubPointer.get_array_field (|
                      x,
                      M.alloc (| Value.Integer IntegerKind.Usize 3 |)
                    |)
                  |);
                  M.read (|
                    M.SubPointer.get_array_field (|
                      x,
                      M.alloc (| Value.Integer IntegerKind.Usize 4 |)
                    |)
                  |);
                  M.read (|
                    M.SubPointer.get_array_field (|
                      x,
                      M.alloc (| Value.Integer IntegerKind.Usize 5 |)
                    |)
                  |);
                  M.read (|
                    M.SubPointer.get_array_field (|
                      x,
                      M.alloc (| Value.Integer IntegerKind.Usize 6 |)
                    |)
                  |);
                  M.read (|
                    M.SubPointer.get_array_field (|
                      x,
                      M.alloc (| Value.Integer IntegerKind.Usize 7 |)
                    |)
                  |)
                ]
            ]
          |)
        |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

Axiom Function_u64_to_address : M.IsFunction "revm_precompile::u64_to_address" u64_to_address.
