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

Module kzg.
  Module trusted_setup_points.
    Definition value_NUM_G1_POINTS : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 4096 |))).
    
    Definition value_NUM_G2_POINTS : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 65 |))).
    
    (* StructTuple
      {
        name := "G1Points";
        const_params := [];
        ty_params := [];
        fields :=
          [
            Ty.apply
              (Ty.path "array")
              [
                M.unevaluated_const
                  (M.get_constant (|
                    "revm_primitives::kzg::trusted_setup_points::G1Points_discriminant"
                  |))
              ]
              [
                Ty.apply
                  (Ty.path "array")
                  [
                    M.unevaluated_const
                      (M.get_constant (|
                        "revm_primitives::kzg::trusted_setup_points::G1Points_discriminant"
                      |))
                  ]
                  [ Ty.path "u8" ]
              ]
          ];
      } *)
    
    Module Impl_core_fmt_Debug_for_revm_primitives_kzg_trusted_setup_points_G1Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G1Points".
      
      (* 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_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "G1Points" |);
                M.alloc (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "revm_primitives::kzg::trusted_setup_points::G1Points",
                    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_trusted_setup_points_G1Points.
    
    Module Impl_core_clone_Clone_for_revm_primitives_kzg_trusted_setup_points_G1Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G1Points".
      
      (* 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_primitives::kzg::trusted_setup_points::G1Points"
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "array")
                      [ Value.Integer IntegerKind.Usize 4096 ]
                      [
                        Ty.apply
                          (Ty.path "array")
                          [ Value.Integer IntegerKind.Usize 48 ]
                          [ Ty.path "u8" ]
                      ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_tuple_field (|
                      M.read (| self |),
                      "revm_primitives::kzg::trusted_setup_points::G1Points",
                      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_trusted_setup_points_G1Points.
    
    Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_kzg_trusted_setup_points_G1Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G1Points".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_revm_primitives_kzg_trusted_setup_points_G1Points.
    
    Module Impl_core_cmp_PartialEq_for_revm_primitives_kzg_trusted_setup_points_G1Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G1Points".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply
                  (Ty.path "array")
                  [ Value.Integer IntegerKind.Usize 4096 ]
                  [
                    Ty.apply
                      (Ty.path "array")
                      [ Value.Integer IntegerKind.Usize 48 ]
                      [ Ty.path "u8" ]
                  ],
                [
                  Ty.apply
                    (Ty.path "array")
                    [ Value.Integer IntegerKind.Usize 4096 ]
                    [
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 48 ]
                        [ Ty.path "u8" ]
                    ]
                ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "revm_primitives::kzg::trusted_setup_points::G1Points",
                  0
                |);
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| other |),
                  "revm_primitives::kzg::trusted_setup_points::G1Points",
                  0
                |)
              ]
            |)))
        | _, _, _ => 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_trusted_setup_points_G1Points.
    
    Module Impl_core_convert_AsRef_array_expr_array_expr_u8_for_revm_primitives_kzg_trusted_setup_points_G1Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G1Points".
      
      (* AsRef *)
      Definition as_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_tuple_field (|
              M.read (| self |),
              "revm_primitives::kzg::trusted_setup_points::G1Points",
              0
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::AsRef"
          Self
          (* Trait polymorphic types *)
          [
            (* T *)
            Ty.apply
              (Ty.path "array")
              [
                M.unevaluated_const
                  (M.get_constant (| "revm_primitives::kzg::trusted_setup_points_discriminant" |))
              ]
              [
                Ty.apply
                  (Ty.path "array")
                  [
                    M.unevaluated_const
                      (M.get_constant (|
                        "revm_primitives::kzg::trusted_setup_points_discriminant"
                      |))
                  ]
                  [ Ty.path "u8" ]
              ]
          ]
          (* Instance *) [ ("as_ref", InstanceField.Method as_ref) ].
    End Impl_core_convert_AsRef_array_expr_array_expr_u8_for_revm_primitives_kzg_trusted_setup_points_G1Points.
    
    Module Impl_core_convert_AsMut_array_expr_array_expr_u8_for_revm_primitives_kzg_trusted_setup_points_G1Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G1Points".
      
      (* AsMut *)
      Definition as_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_tuple_field (|
              M.read (| self |),
              "revm_primitives::kzg::trusted_setup_points::G1Points",
              0
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::AsMut"
          Self
          (* Trait polymorphic types *)
          [
            (* T *)
            Ty.apply
              (Ty.path "array")
              [
                M.unevaluated_const
                  (M.get_constant (| "revm_primitives::kzg::trusted_setup_points_discriminant" |))
              ]
              [
                Ty.apply
                  (Ty.path "array")
                  [
                    M.unevaluated_const
                      (M.get_constant (|
                        "revm_primitives::kzg::trusted_setup_points_discriminant"
                      |))
                  ]
                  [ Ty.path "u8" ]
              ]
          ]
          (* Instance *) [ ("as_mut", InstanceField.Method as_mut) ].
    End Impl_core_convert_AsMut_array_expr_array_expr_u8_for_revm_primitives_kzg_trusted_setup_points_G1Points.
    
    Module Impl_core_ops_deref_Deref_for_revm_primitives_kzg_trusted_setup_points_G1Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G1Points".
      
      (* Deref *)
      Definition _Target : Ty.t :=
        Ty.apply
          (Ty.path "array")
          [
            M.unevaluated_const
              (M.get_constant (|
                "revm_primitives::kzg::trusted_setup_points::Target_discriminant"
              |))
          ]
          [
            Ty.apply
              (Ty.path "array")
              [
                M.unevaluated_const
                  (M.get_constant (|
                    "revm_primitives::kzg::trusted_setup_points::Target_discriminant"
                  |))
              ]
              [ Ty.path "u8" ]
          ].
      
      (* Deref *)
      Definition deref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_tuple_field (|
              M.read (| self |),
              "revm_primitives::kzg::trusted_setup_points::G1Points",
              0
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::deref::Deref"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Target", InstanceField.Ty _Target); ("deref", InstanceField.Method deref) ].
    End Impl_core_ops_deref_Deref_for_revm_primitives_kzg_trusted_setup_points_G1Points.
    
    Module Impl_core_ops_deref_DerefMut_for_revm_primitives_kzg_trusted_setup_points_G1Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G1Points".
      
      (* DerefMut *)
      Definition deref_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_tuple_field (|
              M.read (| self |),
              "revm_primitives::kzg::trusted_setup_points::G1Points",
              0
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::deref::DerefMut"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("deref_mut", InstanceField.Method deref_mut) ].
    End Impl_core_ops_deref_DerefMut_for_revm_primitives_kzg_trusted_setup_points_G1Points.
    
    Module Impl_core_default_Default_for_revm_primitives_kzg_trusted_setup_points_G1Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G1Points".
      
      (*
          fn default() -> Self {
              Self([[0; BYTES_PER_G1_POINT]; NUM_G1_POINTS])
          }
      *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructTuple
              "revm_primitives::kzg::trusted_setup_points::G1Points"
              [
                repeat (|
                  repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 48 |),
                  Value.Integer IntegerKind.Usize 4096
                |)
              ]))
        | _, _, _ => 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_trusted_setup_points_G1Points.
    
    (* StructTuple
      {
        name := "G2Points";
        const_params := [];
        ty_params := [];
        fields :=
          [
            Ty.apply
              (Ty.path "array")
              [
                M.unevaluated_const
                  (M.get_constant (|
                    "revm_primitives::kzg::trusted_setup_points::G2Points_discriminant"
                  |))
              ]
              [
                Ty.apply
                  (Ty.path "array")
                  [
                    M.unevaluated_const
                      (M.get_constant (|
                        "revm_primitives::kzg::trusted_setup_points::G2Points_discriminant"
                      |))
                  ]
                  [ Ty.path "u8" ]
              ]
          ];
      } *)
    
    Module Impl_core_fmt_Debug_for_revm_primitives_kzg_trusted_setup_points_G2Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G2Points".
      
      (* 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_field1_finish",
                []
              |),
              [
                M.read (| f |);
                M.read (| Value.String "G2Points" |);
                M.alloc (|
                  M.SubPointer.get_struct_tuple_field (|
                    M.read (| self |),
                    "revm_primitives::kzg::trusted_setup_points::G2Points",
                    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_trusted_setup_points_G2Points.
    
    Module Impl_core_clone_Clone_for_revm_primitives_kzg_trusted_setup_points_G2Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G2Points".
      
      (* 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_primitives::kzg::trusted_setup_points::G2Points"
              [
                M.call_closure (|
                  M.get_trait_method (|
                    "core::clone::Clone",
                    Ty.apply
                      (Ty.path "array")
                      [ Value.Integer IntegerKind.Usize 65 ]
                      [
                        Ty.apply
                          (Ty.path "array")
                          [ Value.Integer IntegerKind.Usize 96 ]
                          [ Ty.path "u8" ]
                      ],
                    [],
                    "clone",
                    []
                  |),
                  [
                    M.SubPointer.get_struct_tuple_field (|
                      M.read (| self |),
                      "revm_primitives::kzg::trusted_setup_points::G2Points",
                      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_trusted_setup_points_G2Points.
    
    Module Impl_core_cmp_Eq_for_revm_primitives_kzg_trusted_setup_points_G2Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G2Points".
      
      (* 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_trusted_setup_points_G2Points.
    
    Module Impl_core_marker_StructuralPartialEq_for_revm_primitives_kzg_trusted_setup_points_G2Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G2Points".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::marker::StructuralPartialEq"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_marker_StructuralPartialEq_for_revm_primitives_kzg_trusted_setup_points_G2Points.
    
    Module Impl_core_cmp_PartialEq_for_revm_primitives_kzg_trusted_setup_points_G2Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G2Points".
      
      (* PartialEq *)
      Definition eq (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; other ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let other := M.alloc (| other |) in
            M.call_closure (|
              M.get_trait_method (|
                "core::cmp::PartialEq",
                Ty.apply
                  (Ty.path "array")
                  [ Value.Integer IntegerKind.Usize 65 ]
                  [
                    Ty.apply
                      (Ty.path "array")
                      [ Value.Integer IntegerKind.Usize 96 ]
                      [ Ty.path "u8" ]
                  ],
                [
                  Ty.apply
                    (Ty.path "array")
                    [ Value.Integer IntegerKind.Usize 65 ]
                    [
                      Ty.apply
                        (Ty.path "array")
                        [ Value.Integer IntegerKind.Usize 96 ]
                        [ Ty.path "u8" ]
                    ]
                ],
                "eq",
                []
              |),
              [
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| self |),
                  "revm_primitives::kzg::trusted_setup_points::G2Points",
                  0
                |);
                M.SubPointer.get_struct_tuple_field (|
                  M.read (| other |),
                  "revm_primitives::kzg::trusted_setup_points::G2Points",
                  0
                |)
              ]
            |)))
        | _, _, _ => 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_trusted_setup_points_G2Points.
    
    Module Impl_core_convert_AsRef_array_expr_array_expr_u8_for_revm_primitives_kzg_trusted_setup_points_G2Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G2Points".
      
      (* AsRef *)
      Definition as_ref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_tuple_field (|
              M.read (| self |),
              "revm_primitives::kzg::trusted_setup_points::G2Points",
              0
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::AsRef"
          Self
          (* Trait polymorphic types *)
          [
            (* T *)
            Ty.apply
              (Ty.path "array")
              [
                M.unevaluated_const
                  (M.get_constant (| "revm_primitives::kzg::trusted_setup_points_discriminant" |))
              ]
              [
                Ty.apply
                  (Ty.path "array")
                  [
                    M.unevaluated_const
                      (M.get_constant (|
                        "revm_primitives::kzg::trusted_setup_points_discriminant"
                      |))
                  ]
                  [ Ty.path "u8" ]
              ]
          ]
          (* Instance *) [ ("as_ref", InstanceField.Method as_ref) ].
    End Impl_core_convert_AsRef_array_expr_array_expr_u8_for_revm_primitives_kzg_trusted_setup_points_G2Points.
    
    Module Impl_core_convert_AsMut_array_expr_array_expr_u8_for_revm_primitives_kzg_trusted_setup_points_G2Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G2Points".
      
      (* AsMut *)
      Definition as_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_tuple_field (|
              M.read (| self |),
              "revm_primitives::kzg::trusted_setup_points::G2Points",
              0
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::convert::AsMut"
          Self
          (* Trait polymorphic types *)
          [
            (* T *)
            Ty.apply
              (Ty.path "array")
              [
                M.unevaluated_const
                  (M.get_constant (| "revm_primitives::kzg::trusted_setup_points_discriminant" |))
              ]
              [
                Ty.apply
                  (Ty.path "array")
                  [
                    M.unevaluated_const
                      (M.get_constant (|
                        "revm_primitives::kzg::trusted_setup_points_discriminant"
                      |))
                  ]
                  [ Ty.path "u8" ]
              ]
          ]
          (* Instance *) [ ("as_mut", InstanceField.Method as_mut) ].
    End Impl_core_convert_AsMut_array_expr_array_expr_u8_for_revm_primitives_kzg_trusted_setup_points_G2Points.
    
    Module Impl_core_ops_deref_Deref_for_revm_primitives_kzg_trusted_setup_points_G2Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G2Points".
      
      (* Deref *)
      Definition _Target : Ty.t :=
        Ty.apply
          (Ty.path "array")
          [
            M.unevaluated_const
              (M.get_constant (|
                "revm_primitives::kzg::trusted_setup_points::Target_discriminant"
              |))
          ]
          [
            Ty.apply
              (Ty.path "array")
              [
                M.unevaluated_const
                  (M.get_constant (|
                    "revm_primitives::kzg::trusted_setup_points::Target_discriminant"
                  |))
              ]
              [ Ty.path "u8" ]
          ].
      
      (* Deref *)
      Definition deref (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_tuple_field (|
              M.read (| self |),
              "revm_primitives::kzg::trusted_setup_points::G2Points",
              0
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::deref::Deref"
          Self
          (* Trait polymorphic types *) []
          (* Instance *)
          [ ("Target", InstanceField.Ty _Target); ("deref", InstanceField.Method deref) ].
    End Impl_core_ops_deref_Deref_for_revm_primitives_kzg_trusted_setup_points_G2Points.
    
    Module Impl_core_ops_deref_DerefMut_for_revm_primitives_kzg_trusted_setup_points_G2Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G2Points".
      
      (* DerefMut *)
      Definition deref_mut (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            M.SubPointer.get_struct_tuple_field (|
              M.read (| self |),
              "revm_primitives::kzg::trusted_setup_points::G2Points",
              0
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::ops::deref::DerefMut"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("deref_mut", InstanceField.Method deref_mut) ].
    End Impl_core_ops_deref_DerefMut_for_revm_primitives_kzg_trusted_setup_points_G2Points.
    
    Module Impl_core_default_Default_for_revm_primitives_kzg_trusted_setup_points_G2Points.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::G2Points".
      
      (*
          fn default() -> Self {
              Self([[0; BYTES_PER_G2_POINT]; NUM_G2_POINTS])
          }
      *)
      Definition default (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [] =>
          ltac:(M.monadic
            (Value.StructTuple
              "revm_primitives::kzg::trusted_setup_points::G2Points"
              [
                repeat (|
                  repeat (| Value.Integer IntegerKind.U8 0, Value.Integer IntegerKind.Usize 96 |),
                  Value.Integer IntegerKind.Usize 65
                |)
              ]))
        | _, _, _ => 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_trusted_setup_points_G2Points.
    
    Definition value_G1_POINTS : Value.t :=
      M.run
        ltac:(M.monadic
          (let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            BinOp.eq (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                  "len",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.get_constant (|
                                      "revm_primitives::kzg::trusted_setup_points::G1_POINTS::BYTES"
                                    |)
                                  |)
                                ]
                              |),
                              M.call_closure (|
                                M.get_function (|
                                  "core::mem::size_of",
                                  [ Ty.path "revm_primitives::kzg::trusted_setup_points::G1Points" ]
                                |),
                                []
                              |)
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic", [] |),
                          [
                            M.read (|
                              Value.String
                                "assertion failed: BYTES.len() == core::mem::size_of::<G1Points>()"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                "cast",
                [ Ty.path "revm_primitives::kzg::trusted_setup_points::G1Points" ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                    "as_ptr",
                    []
                  |),
                  [
                    M.read (|
                      M.get_constant (|
                        "revm_primitives::kzg::trusted_setup_points::G1_POINTS::BYTES"
                      |)
                    |)
                  ]
                |)
              ]
            |)
          |))).
    
    Module G1_POINTS.
      Definition value_BYTES : Value.t :=
        M.run ltac:(M.monadic (M.alloc (| M.read (| UnsupportedLiteral |) |))).
    End G1_POINTS.
    
    Definition value_G2_POINTS : Value.t :=
      M.run
        ltac:(M.monadic
          (let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          UnOp.not (|
                            BinOp.eq (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                  "len",
                                  []
                                |),
                                [
                                  M.read (|
                                    M.get_constant (|
                                      "revm_primitives::kzg::trusted_setup_points::G2_POINTS::BYTES"
                                    |)
                                  |)
                                ]
                              |),
                              M.call_closure (|
                                M.get_function (|
                                  "core::mem::size_of",
                                  [ Ty.path "revm_primitives::kzg::trusted_setup_points::G2Points" ]
                                |),
                                []
                              |)
                            |)
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.never_to_any (|
                        M.call_closure (|
                          M.get_function (| "core::panicking::panic", [] |),
                          [
                            M.read (|
                              Value.String
                                "assertion failed: BYTES.len() == core::mem::size_of::<G2Points>()"
                            |)
                          ]
                        |)
                      |)
                    |)));
                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
              ]
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
                "cast",
                [ Ty.path "revm_primitives::kzg::trusted_setup_points::G2Points" ]
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                    "as_ptr",
                    []
                  |),
                  [
                    M.read (|
                      M.get_constant (|
                        "revm_primitives::kzg::trusted_setup_points::G2_POINTS::BYTES"
                      |)
                    |)
                  ]
                |)
              ]
            |)
          |))).
    
    Module G2_POINTS.
      Definition value_BYTES : Value.t :=
        M.run ltac:(M.monadic (M.alloc (| M.read (| UnsupportedLiteral |) |))).
    End G2_POINTS.
    
    (*
    pub fn parse_kzg_trusted_setup(
        trusted_setup: &str,
    ) -> Result<(Box<G1Points>, Box<G2Points>), KzgErrors> {
        let mut lines = trusted_setup.lines();
    
        // load number of points
        let n_g1 = lines
            .next()
            .ok_or(KzgErrors::FileFormatError)?
            .parse::<usize>()
            .map_err(|_| KzgErrors::ParseError)?;
        let n_g2 = lines
            .next()
            .ok_or(KzgErrors::FileFormatError)?
            .parse::<usize>()
            .map_err(|_| KzgErrors::ParseError)?;
    
        if n_g1 != NUM_G1_POINTS {
            return Err(KzgErrors::MismatchedNumberOfPoints);
        }
    
        if n_g2 != NUM_G2_POINTS {
            return Err(KzgErrors::MismatchedNumberOfPoints);
        }
    
        // load g1 points
        let mut g1_points = Box::<G1Points>::default();
        for bytes in &mut g1_points.0 {
            let line = lines.next().ok_or(KzgErrors::FileFormatError)?;
            crate::hex::decode_to_slice(line, bytes).map_err(|_| KzgErrors::ParseError)?;
        }
    
        // load g2 points
        let mut g2_points = Box::<G2Points>::default();
        for bytes in &mut g2_points.0 {
            let line = lines.next().ok_or(KzgErrors::FileFormatError)?;
            crate::hex::decode_to_slice(line, bytes).map_err(|_| KzgErrors::ParseError)?;
        }
    
        if lines.next().is_some() {
            return Err(KzgErrors::FileFormatError);
        }
    
        Ok((g1_points, g2_points))
    }
    *)
    Definition parse_kzg_trusted_setup (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ trusted_setup ] =>
        ltac:(M.monadic
          (let trusted_setup := M.alloc (| trusted_setup |) in
          M.catch_return (|
            ltac:(M.monadic
              (M.read (|
                let~ lines :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_associated_function (| Ty.path "str", "lines", [] |),
                      [ M.read (| trusted_setup |) ]
                    |)
                  |) in
                let~ n_g1 :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.path "usize";
                                Ty.path "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  []
                                  [ Ty.path "usize"; Ty.path "core::num::error::ParseIntError" ],
                                "map_err",
                                [
                                  Ty.path "revm_primitives::kzg::trusted_setup_points::KzgErrors";
                                  Ty.function
                                    [ Ty.tuple [ Ty.path "core::num::error::ParseIntError" ] ]
                                    (Ty.path
                                      "revm_primitives::kzg::trusted_setup_points::KzgErrors")
                                ]
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "str",
                                    "parse",
                                    [ Ty.path "usize" ]
                                  |),
                                  [
                                    M.read (|
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::try_trait::Try",
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                []
                                                [
                                                  Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                                                  Ty.path
                                                    "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                ],
                                              [],
                                              "branch",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "core::option::Option")
                                                    []
                                                    [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ],
                                                  "ok_or",
                                                  [
                                                    Ty.path
                                                      "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                  ]
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::iter::traits::iterator::Iterator",
                                                      Ty.path "core::str::iter::Lines",
                                                      [],
                                                      "next",
                                                      []
                                                    |),
                                                    [ lines ]
                                                  |);
                                                  Value.StructTuple
                                                    "revm_primitives::kzg::trusted_setup_points::KzgErrors::FileFormatError"
                                                    []
                                                ]
                                              |)
                                            ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::ops::control_flow::ControlFlow::Break",
                                                  0
                                                |) in
                                              let residual := M.copy (| γ0_0 |) in
                                              M.alloc (|
                                                M.never_to_any (|
                                                  M.read (|
                                                    M.return_ (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::try_trait::FromResidual",
                                                          Ty.apply
                                                            (Ty.path "core::result::Result")
                                                            []
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "alloc::boxed::Box")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "revm_primitives::kzg::trusted_setup_points::G1Points";
                                                                      Ty.path "alloc::alloc::Global"
                                                                    ];
                                                                  Ty.apply
                                                                    (Ty.path "alloc::boxed::Box")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "revm_primitives::kzg::trusted_setup_points::G2Points";
                                                                      Ty.path "alloc::alloc::Global"
                                                                    ]
                                                                ];
                                                              Ty.path
                                                                "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                            ],
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.path "core::convert::Infallible";
                                                                Ty.path
                                                                  "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                              ]
                                                          ],
                                                          "from_residual",
                                                          []
                                                        |),
                                                        [ M.read (| residual |) ]
                                                      |)
                                                    |)
                                                  |)
                                                |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::ops::control_flow::ControlFlow::Continue",
                                                  0
                                                |) in
                                              let val := M.copy (| γ0_0 |) in
                                              val))
                                        ]
                                      |)
                                    |)
                                  ]
                                |);
                                M.closure
                                  (fun γ =>
                                    ltac:(M.monadic
                                      match γ with
                                      | [ α0 ] =>
                                        ltac:(M.monadic
                                          (M.match_operator (|
                                            M.alloc (| α0 |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (Value.StructTuple
                                                    "revm_primitives::kzg::trusted_setup_points::KzgErrors::ParseError"
                                                    []))
                                            ]
                                          |)))
                                      | _ => M.impossible "wrong number of arguments"
                                      end))
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.tuple
                                              [
                                                Ty.apply
                                                  (Ty.path "alloc::boxed::Box")
                                                  []
                                                  [
                                                    Ty.path
                                                      "revm_primitives::kzg::trusted_setup_points::G1Points";
                                                    Ty.path "alloc::alloc::Global"
                                                  ];
                                                Ty.apply
                                                  (Ty.path "alloc::boxed::Box")
                                                  []
                                                  [
                                                    Ty.path
                                                      "revm_primitives::kzg::trusted_setup_points::G2Points";
                                                    Ty.path "alloc::alloc::Global"
                                                  ]
                                              ];
                                            Ty.path
                                              "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path
                                                "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |)
                  |) in
                let~ n_g2 :=
                  M.copy (|
                    M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::ops::try_trait::Try",
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.path "usize";
                                Ty.path "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                              ],
                            [],
                            "branch",
                            []
                          |),
                          [
                            M.call_closure (|
                              M.get_associated_function (|
                                Ty.apply
                                  (Ty.path "core::result::Result")
                                  []
                                  [ Ty.path "usize"; Ty.path "core::num::error::ParseIntError" ],
                                "map_err",
                                [
                                  Ty.path "revm_primitives::kzg::trusted_setup_points::KzgErrors";
                                  Ty.function
                                    [ Ty.tuple [ Ty.path "core::num::error::ParseIntError" ] ]
                                    (Ty.path
                                      "revm_primitives::kzg::trusted_setup_points::KzgErrors")
                                ]
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "str",
                                    "parse",
                                    [ Ty.path "usize" ]
                                  |),
                                  [
                                    M.read (|
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::try_trait::Try",
                                              Ty.apply
                                                (Ty.path "core::result::Result")
                                                []
                                                [
                                                  Ty.apply (Ty.path "&") [] [ Ty.path "str" ];
                                                  Ty.path
                                                    "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                ],
                                              [],
                                              "branch",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.apply
                                                    (Ty.path "core::option::Option")
                                                    []
                                                    [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ],
                                                  "ok_or",
                                                  [
                                                    Ty.path
                                                      "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                  ]
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::iter::traits::iterator::Iterator",
                                                      Ty.path "core::str::iter::Lines",
                                                      [],
                                                      "next",
                                                      []
                                                    |),
                                                    [ lines ]
                                                  |);
                                                  Value.StructTuple
                                                    "revm_primitives::kzg::trusted_setup_points::KzgErrors::FileFormatError"
                                                    []
                                                ]
                                              |)
                                            ]
                                          |)
                                        |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::ops::control_flow::ControlFlow::Break",
                                                  0
                                                |) in
                                              let residual := M.copy (| γ0_0 |) in
                                              M.alloc (|
                                                M.never_to_any (|
                                                  M.read (|
                                                    M.return_ (|
                                                      M.call_closure (|
                                                        M.get_trait_method (|
                                                          "core::ops::try_trait::FromResidual",
                                                          Ty.apply
                                                            (Ty.path "core::result::Result")
                                                            []
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "alloc::boxed::Box")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "revm_primitives::kzg::trusted_setup_points::G1Points";
                                                                      Ty.path "alloc::alloc::Global"
                                                                    ];
                                                                  Ty.apply
                                                                    (Ty.path "alloc::boxed::Box")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "revm_primitives::kzg::trusted_setup_points::G2Points";
                                                                      Ty.path "alloc::alloc::Global"
                                                                    ]
                                                                ];
                                                              Ty.path
                                                                "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                            ],
                                                          [
                                                            Ty.apply
                                                              (Ty.path "core::result::Result")
                                                              []
                                                              [
                                                                Ty.path "core::convert::Infallible";
                                                                Ty.path
                                                                  "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                              ]
                                                          ],
                                                          "from_residual",
                                                          []
                                                        |),
                                                        [ M.read (| residual |) ]
                                                      |)
                                                    |)
                                                  |)
                                                |)
                                              |)));
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let γ0_0 :=
                                                M.SubPointer.get_struct_tuple_field (|
                                                  γ,
                                                  "core::ops::control_flow::ControlFlow::Continue",
                                                  0
                                                |) in
                                              let val := M.copy (| γ0_0 |) in
                                              val))
                                        ]
                                      |)
                                    |)
                                  ]
                                |);
                                M.closure
                                  (fun γ =>
                                    ltac:(M.monadic
                                      match γ with
                                      | [ α0 ] =>
                                        ltac:(M.monadic
                                          (M.match_operator (|
                                            M.alloc (| α0 |),
                                            [
                                              fun γ =>
                                                ltac:(M.monadic
                                                  (Value.StructTuple
                                                    "revm_primitives::kzg::trusted_setup_points::KzgErrors::ParseError"
                                                    []))
                                            ]
                                          |)))
                                      | _ => M.impossible "wrong number of arguments"
                                      end))
                              ]
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Break",
                                0
                              |) in
                            let residual := M.copy (| γ0_0 |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  M.return_ (|
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::try_trait::FromResidual",
                                        Ty.apply
                                          (Ty.path "core::result::Result")
                                          []
                                          [
                                            Ty.tuple
                                              [
                                                Ty.apply
                                                  (Ty.path "alloc::boxed::Box")
                                                  []
                                                  [
                                                    Ty.path
                                                      "revm_primitives::kzg::trusted_setup_points::G1Points";
                                                    Ty.path "alloc::alloc::Global"
                                                  ];
                                                Ty.apply
                                                  (Ty.path "alloc::boxed::Box")
                                                  []
                                                  [
                                                    Ty.path
                                                      "revm_primitives::kzg::trusted_setup_points::G2Points";
                                                    Ty.path "alloc::alloc::Global"
                                                  ]
                                              ];
                                            Ty.path
                                              "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                          ],
                                        [
                                          Ty.apply
                                            (Ty.path "core::result::Result")
                                            []
                                            [
                                              Ty.path "core::convert::Infallible";
                                              Ty.path
                                                "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                            ]
                                        ],
                                        "from_residual",
                                        []
                                      |),
                                      [ M.read (| residual |) ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let γ0_0 :=
                              M.SubPointer.get_struct_tuple_field (|
                                γ,
                                "core::ops::control_flow::ControlFlow::Continue",
                                0
                              |) in
                            let val := M.copy (| γ0_0 |) in
                            val))
                      ]
                    |)
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.ne (|
                                  M.read (| n_g1 |),
                                  M.read (|
                                    M.get_constant (|
                                      "revm_primitives::kzg::trusted_setup_points::NUM_G1_POINTS"
                                    |)
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      Value.StructTuple
                                        "revm_primitives::kzg::trusted_setup_points::KzgErrors::MismatchedNumberOfPoints"
                                        []
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                BinOp.ne (|
                                  M.read (| n_g2 |),
                                  M.read (|
                                    M.get_constant (|
                                      "revm_primitives::kzg::trusted_setup_points::NUM_G2_POINTS"
                                    |)
                                  |)
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      Value.StructTuple
                                        "revm_primitives::kzg::trusted_setup_points::KzgErrors::MismatchedNumberOfPoints"
                                        []
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                let~ g1_points :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.apply
                          (Ty.path "alloc::boxed::Box")
                          []
                          [
                            Ty.path "revm_primitives::kzg::trusted_setup_points::G1Points";
                            Ty.path "alloc::alloc::Global"
                          ],
                        [],
                        "default",
                        []
                      |),
                      []
                    |)
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&mut")
                              []
                              [
                                Ty.apply
                                  (Ty.path "array")
                                  [ Value.Integer IntegerKind.Usize 4096 ]
                                  [
                                    Ty.apply
                                      (Ty.path "array")
                                      [ Value.Integer IntegerKind.Usize 48 ]
                                      [ Ty.path "u8" ]
                                  ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_tuple_field (|
                              M.read (| g1_points |),
                              "revm_primitives::kzg::trusted_setup_points::G1Points",
                              0
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::slice::iter::IterMut")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "array")
                                                [ Value.Integer IntegerKind.Usize 48 ]
                                                [ Ty.path "u8" ]
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let bytes := M.copy (| γ0_0 |) in
                                          let~ line :=
                                            M.copy (|
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::Try",
                                                      Ty.apply
                                                        (Ty.path "core::result::Result")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path "&")
                                                            []
                                                            [ Ty.path "str" ];
                                                          Ty.path
                                                            "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                        ],
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "core::option::Option")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [ Ty.path "str" ]
                                                            ],
                                                          "ok_or",
                                                          [
                                                            Ty.path
                                                              "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                          ]
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::iter::traits::iterator::Iterator",
                                                              Ty.path "core::str::iter::Lines",
                                                              [],
                                                              "next",
                                                              []
                                                            |),
                                                            [ lines ]
                                                          |);
                                                          Value.StructTuple
                                                            "revm_primitives::kzg::trusted_setup_points::KzgErrors::FileFormatError"
                                                            []
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Break",
                                                          0
                                                        |) in
                                                      let residual := M.copy (| γ0_0 |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::try_trait::FromResidual",
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    []
                                                                    [
                                                                      Ty.tuple
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "alloc::boxed::Box")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "revm_primitives::kzg::trusted_setup_points::G1Points";
                                                                              Ty.path
                                                                                "alloc::alloc::Global"
                                                                            ];
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "alloc::boxed::Box")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "revm_primitives::kzg::trusted_setup_points::G2Points";
                                                                              Ty.path
                                                                                "alloc::alloc::Global"
                                                                            ]
                                                                        ];
                                                                      Ty.path
                                                                        "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                                    ],
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::result::Result")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "core::convert::Infallible";
                                                                        Ty.path
                                                                          "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                                      ]
                                                                  ],
                                                                  "from_residual",
                                                                  []
                                                                |),
                                                                [ M.read (| residual |) ]
                                                              |)
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Continue",
                                                          0
                                                        |) in
                                                      let val := M.copy (| γ0_0 |) in
                                                      val))
                                                ]
                                              |)
                                            |) in
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::try_trait::Try",
                                                    Ty.apply
                                                      (Ty.path "core::result::Result")
                                                      []
                                                      [
                                                        Ty.tuple [];
                                                        Ty.path
                                                          "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                      ],
                                                    [],
                                                    "branch",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "core::result::Result")
                                                          []
                                                          [
                                                            Ty.tuple [];
                                                            Ty.path "const_hex::error::FromHexError"
                                                          ],
                                                        "map_err",
                                                        [
                                                          Ty.path
                                                            "revm_primitives::kzg::trusted_setup_points::KzgErrors";
                                                          Ty.function
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.path
                                                                    "const_hex::error::FromHexError"
                                                                ]
                                                            ]
                                                            (Ty.path
                                                              "revm_primitives::kzg::trusted_setup_points::KzgErrors")
                                                        ]
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "const_hex::decode_to_slice",
                                                            [
                                                              Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [ Ty.path "str" ]
                                                            ]
                                                          |),
                                                          [ M.read (| line |); M.read (| bytes |) ]
                                                        |);
                                                        M.closure
                                                          (fun γ =>
                                                            ltac:(M.monadic
                                                              match γ with
                                                              | [ α0 ] =>
                                                                ltac:(M.monadic
                                                                  (M.match_operator (|
                                                                    M.alloc (| α0 |),
                                                                    [
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (Value.StructTuple
                                                                            "revm_primitives::kzg::trusted_setup_points::KzgErrors::ParseError"
                                                                            []))
                                                                    ]
                                                                  |)))
                                                              | _ =>
                                                                M.impossible
                                                                  "wrong number of arguments"
                                                              end))
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::ops::control_flow::ControlFlow::Break",
                                                        0
                                                      |) in
                                                    let residual := M.copy (| γ0_0 |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          M.return_ (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::try_trait::FromResidual",
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.tuple
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "alloc::boxed::Box")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "revm_primitives::kzg::trusted_setup_points::G1Points";
                                                                            Ty.path
                                                                              "alloc::alloc::Global"
                                                                          ];
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "alloc::boxed::Box")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "revm_primitives::kzg::trusted_setup_points::G2Points";
                                                                            Ty.path
                                                                              "alloc::alloc::Global"
                                                                          ]
                                                                      ];
                                                                    Ty.path
                                                                      "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                                  ],
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "core::convert::Infallible";
                                                                      Ty.path
                                                                        "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                                    ]
                                                                ],
                                                                "from_residual",
                                                                []
                                                              |),
                                                              [ M.read (| residual |) ]
                                                            |)
                                                          |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::ops::control_flow::ControlFlow::Continue",
                                                        0
                                                      |) in
                                                    let val := M.copy (| γ0_0 |) in
                                                    val))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ g2_points :=
                  M.alloc (|
                    M.call_closure (|
                      M.get_trait_method (|
                        "core::default::Default",
                        Ty.apply
                          (Ty.path "alloc::boxed::Box")
                          []
                          [
                            Ty.path "revm_primitives::kzg::trusted_setup_points::G2Points";
                            Ty.path "alloc::alloc::Global"
                          ],
                        [],
                        "default",
                        []
                      |),
                      []
                    |)
                  |) in
                let~ _ :=
                  M.use
                    (M.match_operator (|
                      M.alloc (|
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::iter::traits::collect::IntoIterator",
                            Ty.apply
                              (Ty.path "&mut")
                              []
                              [
                                Ty.apply
                                  (Ty.path "array")
                                  [ Value.Integer IntegerKind.Usize 65 ]
                                  [
                                    Ty.apply
                                      (Ty.path "array")
                                      [ Value.Integer IntegerKind.Usize 96 ]
                                      [ Ty.path "u8" ]
                                  ]
                              ],
                            [],
                            "into_iter",
                            []
                          |),
                          [
                            M.SubPointer.get_struct_tuple_field (|
                              M.read (| g2_points |),
                              "revm_primitives::kzg::trusted_setup_points::G2Points",
                              0
                            |)
                          ]
                        |)
                      |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let iter := M.copy (| γ |) in
                            M.loop (|
                              ltac:(M.monadic
                                (let~ _ :=
                                  M.match_operator (|
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.apply
                                            (Ty.path "core::slice::iter::IterMut")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "array")
                                                [ Value.Integer IntegerKind.Usize 96 ]
                                                [ Ty.path "u8" ]
                                            ],
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ iter ]
                                      |)
                                    |),
                                    [
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let _ :=
                                            M.is_struct_tuple (|
                                              γ,
                                              "core::option::Option::None"
                                            |) in
                                          M.alloc (|
                                            M.never_to_any (| M.read (| M.break (||) |) |)
                                          |)));
                                      fun γ =>
                                        ltac:(M.monadic
                                          (let γ0_0 :=
                                            M.SubPointer.get_struct_tuple_field (|
                                              γ,
                                              "core::option::Option::Some",
                                              0
                                            |) in
                                          let bytes := M.copy (| γ0_0 |) in
                                          let~ line :=
                                            M.copy (|
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::try_trait::Try",
                                                      Ty.apply
                                                        (Ty.path "core::result::Result")
                                                        []
                                                        [
                                                          Ty.apply
                                                            (Ty.path "&")
                                                            []
                                                            [ Ty.path "str" ];
                                                          Ty.path
                                                            "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                        ],
                                                      [],
                                                      "branch",
                                                      []
                                                    |),
                                                    [
                                                      M.call_closure (|
                                                        M.get_associated_function (|
                                                          Ty.apply
                                                            (Ty.path "core::option::Option")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [ Ty.path "str" ]
                                                            ],
                                                          "ok_or",
                                                          [
                                                            Ty.path
                                                              "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                          ]
                                                        |),
                                                        [
                                                          M.call_closure (|
                                                            M.get_trait_method (|
                                                              "core::iter::traits::iterator::Iterator",
                                                              Ty.path "core::str::iter::Lines",
                                                              [],
                                                              "next",
                                                              []
                                                            |),
                                                            [ lines ]
                                                          |);
                                                          Value.StructTuple
                                                            "revm_primitives::kzg::trusted_setup_points::KzgErrors::FileFormatError"
                                                            []
                                                        ]
                                                      |)
                                                    ]
                                                  |)
                                                |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Break",
                                                          0
                                                        |) in
                                                      let residual := M.copy (| γ0_0 |) in
                                                      M.alloc (|
                                                        M.never_to_any (|
                                                          M.read (|
                                                            M.return_ (|
                                                              M.call_closure (|
                                                                M.get_trait_method (|
                                                                  "core::ops::try_trait::FromResidual",
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    []
                                                                    [
                                                                      Ty.tuple
                                                                        [
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "alloc::boxed::Box")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "revm_primitives::kzg::trusted_setup_points::G1Points";
                                                                              Ty.path
                                                                                "alloc::alloc::Global"
                                                                            ];
                                                                          Ty.apply
                                                                            (Ty.path
                                                                              "alloc::boxed::Box")
                                                                            []
                                                                            [
                                                                              Ty.path
                                                                                "revm_primitives::kzg::trusted_setup_points::G2Points";
                                                                              Ty.path
                                                                                "alloc::alloc::Global"
                                                                            ]
                                                                        ];
                                                                      Ty.path
                                                                        "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                                    ],
                                                                  [
                                                                    Ty.apply
                                                                      (Ty.path
                                                                        "core::result::Result")
                                                                      []
                                                                      [
                                                                        Ty.path
                                                                          "core::convert::Infallible";
                                                                        Ty.path
                                                                          "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                                      ]
                                                                  ],
                                                                  "from_residual",
                                                                  []
                                                                |),
                                                                [ M.read (| residual |) ]
                                                              |)
                                                            |)
                                                          |)
                                                        |)
                                                      |)));
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let γ0_0 :=
                                                        M.SubPointer.get_struct_tuple_field (|
                                                          γ,
                                                          "core::ops::control_flow::ControlFlow::Continue",
                                                          0
                                                        |) in
                                                      let val := M.copy (| γ0_0 |) in
                                                      val))
                                                ]
                                              |)
                                            |) in
                                          let~ _ :=
                                            M.match_operator (|
                                              M.alloc (|
                                                M.call_closure (|
                                                  M.get_trait_method (|
                                                    "core::ops::try_trait::Try",
                                                    Ty.apply
                                                      (Ty.path "core::result::Result")
                                                      []
                                                      [
                                                        Ty.tuple [];
                                                        Ty.path
                                                          "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                      ],
                                                    [],
                                                    "branch",
                                                    []
                                                  |),
                                                  [
                                                    M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "core::result::Result")
                                                          []
                                                          [
                                                            Ty.tuple [];
                                                            Ty.path "const_hex::error::FromHexError"
                                                          ],
                                                        "map_err",
                                                        [
                                                          Ty.path
                                                            "revm_primitives::kzg::trusted_setup_points::KzgErrors";
                                                          Ty.function
                                                            [
                                                              Ty.tuple
                                                                [
                                                                  Ty.path
                                                                    "const_hex::error::FromHexError"
                                                                ]
                                                            ]
                                                            (Ty.path
                                                              "revm_primitives::kzg::trusted_setup_points::KzgErrors")
                                                        ]
                                                      |),
                                                      [
                                                        M.call_closure (|
                                                          M.get_function (|
                                                            "const_hex::decode_to_slice",
                                                            [
                                                              Ty.apply
                                                                (Ty.path "&")
                                                                []
                                                                [ Ty.path "str" ]
                                                            ]
                                                          |),
                                                          [ M.read (| line |); M.read (| bytes |) ]
                                                        |);
                                                        M.closure
                                                          (fun γ =>
                                                            ltac:(M.monadic
                                                              match γ with
                                                              | [ α0 ] =>
                                                                ltac:(M.monadic
                                                                  (M.match_operator (|
                                                                    M.alloc (| α0 |),
                                                                    [
                                                                      fun γ =>
                                                                        ltac:(M.monadic
                                                                          (Value.StructTuple
                                                                            "revm_primitives::kzg::trusted_setup_points::KzgErrors::ParseError"
                                                                            []))
                                                                    ]
                                                                  |)))
                                                              | _ =>
                                                                M.impossible
                                                                  "wrong number of arguments"
                                                              end))
                                                      ]
                                                    |)
                                                  ]
                                                |)
                                              |),
                                              [
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::ops::control_flow::ControlFlow::Break",
                                                        0
                                                      |) in
                                                    let residual := M.copy (| γ0_0 |) in
                                                    M.alloc (|
                                                      M.never_to_any (|
                                                        M.read (|
                                                          M.return_ (|
                                                            M.call_closure (|
                                                              M.get_trait_method (|
                                                                "core::ops::try_trait::FromResidual",
                                                                Ty.apply
                                                                  (Ty.path "core::result::Result")
                                                                  []
                                                                  [
                                                                    Ty.tuple
                                                                      [
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "alloc::boxed::Box")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "revm_primitives::kzg::trusted_setup_points::G1Points";
                                                                            Ty.path
                                                                              "alloc::alloc::Global"
                                                                          ];
                                                                        Ty.apply
                                                                          (Ty.path
                                                                            "alloc::boxed::Box")
                                                                          []
                                                                          [
                                                                            Ty.path
                                                                              "revm_primitives::kzg::trusted_setup_points::G2Points";
                                                                            Ty.path
                                                                              "alloc::alloc::Global"
                                                                          ]
                                                                      ];
                                                                    Ty.path
                                                                      "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                                  ],
                                                                [
                                                                  Ty.apply
                                                                    (Ty.path "core::result::Result")
                                                                    []
                                                                    [
                                                                      Ty.path
                                                                        "core::convert::Infallible";
                                                                      Ty.path
                                                                        "revm_primitives::kzg::trusted_setup_points::KzgErrors"
                                                                    ]
                                                                ],
                                                                "from_residual",
                                                                []
                                                              |),
                                                              [ M.read (| residual |) ]
                                                            |)
                                                          |)
                                                        |)
                                                      |)
                                                    |)));
                                                fun γ =>
                                                  ltac:(M.monadic
                                                    (let γ0_0 :=
                                                      M.SubPointer.get_struct_tuple_field (|
                                                        γ,
                                                        "core::ops::control_flow::ControlFlow::Continue",
                                                        0
                                                      |) in
                                                    let val := M.copy (| γ0_0 |) in
                                                    val))
                                              ]
                                            |) in
                                          M.alloc (| Value.Tuple [] |)))
                                    ]
                                  |) in
                                M.alloc (| Value.Tuple [] |)))
                            |)))
                      ]
                    |)) in
                let~ _ :=
                  M.match_operator (|
                    M.alloc (| Value.Tuple [] |),
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ :=
                            M.use
                              (M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "core::option::Option")
                                      []
                                      [ Ty.apply (Ty.path "&") [] [ Ty.path "str" ] ],
                                    "is_some",
                                    []
                                  |),
                                  [
                                    M.alloc (|
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::iter::traits::iterator::Iterator",
                                          Ty.path "core::str::iter::Lines",
                                          [],
                                          "next",
                                          []
                                        |),
                                        [ lines ]
                                      |)
                                    |)
                                  ]
                                |)
                              |)) in
                          let _ :=
                            M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                          M.alloc (|
                            M.never_to_any (|
                              M.read (|
                                M.return_ (|
                                  Value.StructTuple
                                    "core::result::Result::Err"
                                    [
                                      Value.StructTuple
                                        "revm_primitives::kzg::trusted_setup_points::KzgErrors::FileFormatError"
                                        []
                                    ]
                                |)
                              |)
                            |)
                          |)));
                      fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                    ]
                  |) in
                M.alloc (|
                  Value.StructTuple
                    "core::result::Result::Ok"
                    [ Value.Tuple [ M.read (| g1_points |); M.read (| g2_points |) ] ]
                |)
              |)))
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_parse_kzg_trusted_setup :
      M.IsFunction
        "revm_primitives::kzg::trusted_setup_points::parse_kzg_trusted_setup"
        parse_kzg_trusted_setup.
    
    (*
    Enum KzgErrors
    {
      const_params := [];
      ty_params := [];
      variants :=
        [
          {
            name := "FailedCurrentDirectory";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "PathNotExists";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "IOError";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "NotValidFile";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "FileFormatError";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "ParseError";
            item := StructTuple [];
            discriminant := None;
          };
          {
            name := "MismatchedNumberOfPoints";
            item := StructTuple [];
            discriminant := None;
          }
        ];
    }
    *)
    
    Module Impl_core_fmt_Debug_for_revm_primitives_kzg_trusted_setup_points_KzgErrors.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::KzgErrors".
      
      (* Debug *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.call_closure (|
              M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
              [
                M.read (| f |);
                M.read (|
                  M.match_operator (|
                    self,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::FailedCurrentDirectory"
                            |) in
                          M.alloc (| M.read (| Value.String "FailedCurrentDirectory" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::PathNotExists"
                            |) in
                          M.alloc (| M.read (| Value.String "PathNotExists" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::IOError"
                            |) in
                          M.alloc (| M.read (| Value.String "IOError" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::NotValidFile"
                            |) in
                          M.alloc (| M.read (| Value.String "NotValidFile" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::FileFormatError"
                            |) in
                          M.alloc (| M.read (| Value.String "FileFormatError" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::ParseError"
                            |) in
                          M.alloc (| M.read (| Value.String "ParseError" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::MismatchedNumberOfPoints"
                            |) in
                          M.alloc (| M.read (| Value.String "MismatchedNumberOfPoints" |) |)))
                    ]
                  |)
                |)
              ]
            |)))
        | _, _, _ => 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_trusted_setup_points_KzgErrors.
    
    Module Impl_core_fmt_Display_for_revm_primitives_kzg_trusted_setup_points_KzgErrors.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::KzgErrors".
      
      (*
          fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
              let s = match self {
                  Self::FailedCurrentDirectory => "failed to get current directory",
                  Self::PathNotExists => "the specified path does not exist",
                  Self::IOError => "IO error",
                  Self::NotValidFile => "not a valid file",
                  Self::FileFormatError => "file is not properly formatted",
                  Self::ParseError => "could not parse as usize",
                  Self::MismatchedNumberOfPoints => "number of points does not match what is expected",
              };
              f.write_str(s)
          }
      *)
      Definition fmt (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
        match ε, τ, α with
        | [], [], [ self; f ] =>
          ltac:(M.monadic
            (let self := M.alloc (| self |) in
            let f := M.alloc (| f |) in
            M.read (|
              let~ s :=
                M.copy (|
                  M.match_operator (|
                    self,
                    [
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::FailedCurrentDirectory"
                            |) in
                          Value.String "failed to get current directory"));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::PathNotExists"
                            |) in
                          M.alloc (|
                            M.read (| Value.String "the specified path does not exist" |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::IOError"
                            |) in
                          M.alloc (| M.read (| Value.String "IO error" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::NotValidFile"
                            |) in
                          M.alloc (| M.read (| Value.String "not a valid file" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::FileFormatError"
                            |) in
                          M.alloc (|
                            M.read (| Value.String "file is not properly formatted" |)
                          |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::ParseError"
                            |) in
                          M.alloc (| M.read (| Value.String "could not parse as usize" |) |)));
                      fun γ =>
                        ltac:(M.monadic
                          (let γ := M.read (| γ |) in
                          let _ :=
                            M.is_struct_tuple (|
                              γ,
                              "revm_primitives::kzg::trusted_setup_points::KzgErrors::MismatchedNumberOfPoints"
                            |) in
                          M.alloc (|
                            M.read (|
                              Value.String "number of points does not match what is expected"
                            |)
                          |)))
                    ]
                  |)
                |) in
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (| Ty.path "core::fmt::Formatter", "write_str", [] |),
                  [ M.read (| f |); M.read (| s |) ]
                |)
              |)
            |)))
        | _, _, _ => M.impossible "wrong number of arguments"
        end.
      
      Axiom Implements :
        M.IsTraitInstance
          "core::fmt::Display"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [ ("fmt", InstanceField.Method fmt) ].
    End Impl_core_fmt_Display_for_revm_primitives_kzg_trusted_setup_points_KzgErrors.
    
    Module Impl_core_error_Error_for_revm_primitives_kzg_trusted_setup_points_KzgErrors.
      Definition Self : Ty.t := Ty.path "revm_primitives::kzg::trusted_setup_points::KzgErrors".
      
      Axiom Implements :
        M.IsTraitInstance
          "core::error::Error"
          Self
          (* Trait polymorphic types *) []
          (* Instance *) [].
    End Impl_core_error_Error_for_revm_primitives_kzg_trusted_setup_points_KzgErrors.
  End trusted_setup_points.
End kzg.
