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

Module kzg.
  Module env_settings.
    (*
    Enum EnvKzgSettings
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "Default";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "Custom";
            item :=
              StructTuple
                [
                  Ty.apply
                    (Ty.path "alloc::sync::Arc")
                    []
                    [ Ty.path "c_kzg::bindings::KZGSettings"; Ty.path "alloc::alloc::Global" ]
                ];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_fmt_Debug_for_revm_primitives_kzg_env_settings_EnvKzgSettings.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::env_settings::EnvKzgSettings".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Default"
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "write_str",
                            []
                          |),
                          [ M.read (| f |); M.read (| Value.String "Default" |) ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Custom",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.path "core::fmt::Formatter",
                            "debug_tuple_field1_finish",
                            []
                          |),
                          [ M.read (| f |); M.read (| Value.String "Custom" |); __self_0 ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Debug"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Debug_for_revm_primitives_kzg_env_settings_EnvKzgSettings.
    
    Module Impl_core_clone_Clone_for_revm_primitives_kzg_env_settings_EnvKzgSettings.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::env_settings::EnvKzgSettings".
      
      (* Clone *)
      Definition clone (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Default"
                        |) in
                      M.alloc (|
                        Value.StructTuple
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Default"
                          []
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Custom",
                          0
                        |) in
                      let __self_0 := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        Value.StructTuple
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Custom"
                          [
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::clone::Clone",
                                Ty.apply
                                  (Ty.path "alloc::sync::Arc")
                                  []
                                  [
                                    Ty.path "c_kzg::bindings::KZGSettings";
                                    Ty.path "alloc::alloc::Global"
                                  ],
                                [],
                                "clone",
                                []
                              |),
                              [ M.read (| __self_0 |) ]
                            |)
                          ]
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::clone::Clone"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("clone", InstanceField.Method clone) ].
    End Impl_core_clone_Clone_for_revm_primitives_kzg_env_settings_EnvKzgSettings.
    
    Module Impl_core_default_Default_for_revm_primitives_kzg_env_settings_EnvKzgSettings.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::env_settings::EnvKzgSettings".
      
      (* Default *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructTuple "revm_primitives::kzg::env_settings::EnvKzgSettings::Default" []))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::default::Default"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("default", InstanceField.Method default) ].
    End Impl_core_default_Default_for_revm_primitives_kzg_env_settings_EnvKzgSettings.
    
    Module Impl_core_cmp_Eq_for_revm_primitives_kzg_env_settings_EnvKzgSettings.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::env_settings::EnvKzgSettings".
      
      (* Eq *)
      Definition assert_receiver_is_total_eq
          (ε : list Value.t)
          (τ : list Ty.t)
          (α : list Value.t)
          : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                Value.DeclaredButUndefined,
                [ fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |))) ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::Eq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("assert_receiver_is_total_eq", InstanceField.Method assert_receiver_is_total_eq) ].
    End Impl_core_cmp_Eq_for_revm_primitives_kzg_env_settings_EnvKzgSettings.
    
    Module Impl_core_cmp_PartialEq_for_revm_primitives_kzg_env_settings_EnvKzgSettings.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::env_settings::EnvKzgSettings".
      
      (*
          fn eq(&self, other: &Self) -> bool {
              match (self, other) {
                  (Self::Default, Self::Default) => true,
                  (Self::Custom(a), Self::Custom(b)) => Arc::ptr_eq(a, b),
                  _ => false,
              }
          }
      *)
      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 (|
              M.match_operator (|
                M.alloc (| Value.Tuple [ M.read (| self |); M.read (| other |) ] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let γ0_0 := M.read (| γ0_0 |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ0_0,
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Default"
                        |) in
                      let γ0_1 := M.read (| γ0_1 |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ0_1,
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Default"
                        |) in
                      M.alloc (| Value.Bool true |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                      let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                      let γ0_0 := M.read (| γ0_0 |) in
                      let γ2_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ0_0,
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Custom",
                          0
                        |) in
                      let a := M.alloc (| γ2_0 |) in
                      let γ0_1 := M.read (| γ0_1 |) in
                      let γ2_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ0_1,
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Custom",
                          0
                        |) in
                      let b := M.alloc (| γ2_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "alloc::sync::Arc")
                              []
                              [
                                Ty.path "c_kzg::bindings::KZGSettings";
                                Ty.path "alloc::alloc::Global"
                              ],
                            "ptr_eq",
                            []
                          |),
                          [ M.read (| a |); M.read (| b |) ]
                        |)
                      |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Bool false |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::cmp::PartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("eq", InstanceField.Method eq) ].
    End Impl_core_cmp_PartialEq_for_revm_primitives_kzg_env_settings_EnvKzgSettings.
    
    Module Impl_core_hash_Hash_for_revm_primitives_kzg_env_settings_EnvKzgSettings.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::env_settings::EnvKzgSettings".
      
      (*
          fn hash<H: Hasher>(&self, state: &mut H) {
              core::mem::discriminant(self).hash(state);
              match self {
                  Self::Default => {}
                  Self::Custom(settings) => Arc::as_ptr(settings).hash(state),
              }
          }
      *)
      Definition hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [ H ], [ self; state ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let state := M.alloc (| state |) in
            M.read (|
              let~ _ :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::hash::Hash",
                      Ty.apply
                        (Ty.path "core::mem::Discriminant")
                        []
                        [ Ty.path "revm_primitives::kzg::env_settings::EnvKzgSettings" ],
                      [],
                      "hash",
                      [ H ]
                    |),
                    [
                      M.alloc (|
                        M.call_closure (|
                          M.get_function (|
                            "core::mem::discriminant",
                            [ Ty.path "revm_primitives::kzg::env_settings::EnvKzgSettings" ]
                          |),
                          [ M.read (| self |) ]
                        |)
                      |);
                      M.read (| state |)
                    ]
                  |)
                |) in
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Default"
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Custom",
                          0
                        |) in
                      let settings := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::hash::Hash",
                            Ty.apply
                              (Ty.path "*const")
                              []
                              [ Ty.path "c_kzg::bindings::KZGSettings" ],
                            [],
                            "hash",
                            [ H ]
                          |),
                          [
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "alloc::sync::Arc")
                                    []
                                    [
                                      Ty.path "c_kzg::bindings::KZGSettings";
                                      Ty.path "alloc::alloc::Global"
                                    ],
                                  "as_ptr",
                                  []
                                |),
                                [ M.read (| settings |) ]
                              |)
                            |);
                            M.read (| state |)
                          ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::hash::Hash"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("hash", InstanceField.Method hash) ].
    End Impl_core_hash_Hash_for_revm_primitives_kzg_env_settings_EnvKzgSettings.
    
    Module Impl_revm_primitives_kzg_env_settings_EnvKzgSettings.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::env_settings::EnvKzgSettings".
      
      (*
          pub fn get(&self) -> &KzgSettings {
              match self {
                  Self::Default => {
                      static DEFAULT: OnceBox<KzgSettings> = OnceBox::new();
                      DEFAULT.get_or_init(|| {
                          let settings =
                              KzgSettings::load_trusted_setup(G1_POINTS.as_ref(), G2_POINTS.as_ref())
                                  .expect("failed to load default trusted setup");
                          Box::new(settings)
                      })
                  }
                  Self::Custom(settings) => settings,
              }
          }
      *)
      Definition get (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.read (|
              M.match_operator (|
                self,
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let _ :=
                        M.is_struct_tuple (|
                          γ,
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Default"
                        |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "once_cell::race::once_box::OnceBox")
                              []
                              [ Ty.path "c_kzg::bindings::KZGSettings" ],
                            "get_or_init",
                            [
                              Ty.function
                                [ Ty.tuple [] ]
                                (Ty.apply
                                  (Ty.path "alloc::boxed::Box")
                                  []
                                  [
                                    Ty.path "c_kzg::bindings::KZGSettings";
                                    Ty.path "alloc::alloc::Global"
                                  ])
                            ]
                          |),
                          [
                            M.read (|
                              M.get_constant (|
                                "revm_primitives::kzg::env_settings::get::DEFAULT"
                              |)
                            |);
                            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~ settings :=
                                                  M.alloc (|
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "core::result::Result")
                                                          []
                                                          [
                                                            Ty.path "c_kzg::bindings::KZGSettings";
                                                            Ty.path "c_kzg::bindings::Error"
                                                          ],
                                                        "expect",
                                                        []
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path "c_kzg::bindings::KZGSettings",
                                                            "load_trusted_setup",
                                                            []
                                                          |),
                                                          [
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::convert::AsRef",
                                                                Ty.path
                                                                  "revm_primitives::kzg::trusted_setup_points::G1Points",
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "array")
                                                                    [
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        4096
                                                                    ]
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path "array")
                                                                        [
                                                                          Value.Integer
                                                                            IntegerKind.Usize
                                                                            48
                                                                        ]
                                                                        [ Ty.path "u8" ]
                                                                    ]
                                                                ],
                                                                "as_ref",
                                                                []
                                                              |),
                                                              [
                                                                M.read (|
                                                                  M.get_constant (|
                                                                    "revm_primitives::kzg::trusted_setup_points::G1_POINTS"
                                                                  |)
                                                                |)
                                                              ]
                                                            |);
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::convert::AsRef",
                                                                Ty.path
                                                                  "revm_primitives::kzg::trusted_setup_points::G2Points",
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "array")
                                                                    [
                                                                      Value.Integer
                                                                        IntegerKind.Usize
                                                                        65
                                                                    ]
                                                                    [
                                                                      Ty.apply
                                                                        (Ty.path "array")
                                                                        [
                                                                          Value.Integer
                                                                            IntegerKind.Usize
                                                                            96
                                                                        ]
                                                                        [ Ty.path "u8" ]
                                                                    ]
                                                                ],
                                                                "as_ref",
                                                                []
                                                              |),
                                                              [
                                                                M.read (|
                                                                  M.get_constant (|
                                                                    "revm_primitives::kzg::trusted_setup_points::G2_POINTS"
                                                                  |)
                                                                |)
                                                              ]
                                                            |)
                                                          ]
                                                        |);
                                                        M.read (|
                                                          Value.String
                                                            "failed to load default trusted setup"
                                                        |)
                                                      ]
                                                    |)
                                                  |) in
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "alloc::boxed::Box")
                                                        []
                                                        [
                                                          Ty.path "c_kzg::bindings::KZGSettings";
                                                          Ty.path "alloc::alloc::Global"
                                                        ],
                                                      "new",
                                                      []
                                                    |),
                                                    [ M.read (| settings |) ]
                                                  |)
                                                |)
                                              |)))
                                        ]
                                      |)))
                                  | _ => M.impossible "wrong number of arguments"
                                  end))
                          ]
                        |)
                      |)));
                  fun γ =>
                    ltac:(M.monadic
                      (let γ := M.read (| γ |) in
                      let γ1_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "revm_primitives::kzg::env_settings::EnvKzgSettings::Custom",
                          0
                        |) in
                      let settings := M.alloc (| γ1_0 |) in
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::deref::Deref",
                            Ty.apply
                              (Ty.path "alloc::sync::Arc")
                              []
                              [
                                Ty.path "c_kzg::bindings::KZGSettings";
                                Ty.path "alloc::alloc::Global"
                              ],
                            [],
                            "deref",
                            []
                          |),
                          [ M.read (| settings |) ]
                        |)
                      |)))
                ]
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom AssociatedFunction_get : M.IsAssociatedFunction Self "get" get.
    End Impl_revm_primitives_kzg_env_settings_EnvKzgSettings.
  End env_settings.
End kzg.
