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

Module kzg_point_evaluation.
  Definition value_POINT_EVALUATION : Value.t :=
    M.run
      ltac:(M.monadic
        (M.alloc (|
          Value.StructTuple
            "revm_precompile::PrecompileWithAddress"
            [
              M.read (| M.get_constant (| "revm_precompile::kzg_point_evaluation::ADDRESS" |) |);
              Value.StructTuple
                "revm_primitives::precompile::Precompile::Env"
                [
                  (* ReifyFnPointer *)
                  M.pointer_coercion
                    (M.get_function (| "revm_precompile::kzg_point_evaluation::run", [] |))
                ]
            ]
        |))).
  
  Definition value_ADDRESS : Value.t :=
    M.run
      ltac:(M.monadic
        (M.alloc (|
          M.call_closure (|
            M.get_function (| "revm_precompile::u64_to_address", [] |),
            [ Value.Integer IntegerKind.U64 10 ]
          |)
        |))).
  
  Definition value_GAS_COST : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U64 50000 |))).
  
  Definition value_VERSIONED_HASH_VERSION_KZG : Value.t :=
    M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.U8 1 |))).
  
  Definition value_RETURN_VALUE : Value.t :=
    M.run
      ltac:(M.monadic
        (M.alloc (|
          M.get_constant (| "revm_precompile::kzg_point_evaluation::RETURN_VALUE::RES" |)
        |))).
  
  (*
  pub fn run(input: &Bytes, gas_limit: u64, env: &Env) -> PrecompileResult {
      if gas_limit < GAS_COST {
          return Err(Error::OutOfGas);
      }
  
      // Verify input length.
      if input.len() != 192 {
          return Err(Error::BlobInvalidInputLength);
      }
  
      // Verify commitment matches versioned_hash
      let versioned_hash = &input[..32];
      let commitment = &input[96..144];
      if kzg_to_versioned_hash(commitment) != versioned_hash {
          return Err(Error::BlobMismatchedVersion);
      }
  
      // Verify KZG proof with z and y in big endian format
      let commitment = as_bytes48(commitment);
      let z = as_bytes32(&input[32..64]);
      let y = as_bytes32(&input[64..96]);
      let proof = as_bytes48(&input[144..192]);
      if !verify_kzg_proof(commitment, z, y, proof, env.cfg.kzg_settings.get()) {
          return Err(Error::BlobVerifyKzgProofFailed);
      }
  
      // Return FIELD_ELEMENTS_PER_BLOB and BLS_MODULUS as padded 32 byte big endian values
      Ok((GAS_COST, RETURN_VALUE.into()))
  }
  *)
  Definition run (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ input; gas_limit; env ] =>
      ltac:(M.monadic
        (let input := M.alloc (| input |) in
        let gas_limit := M.alloc (| gas_limit |) in
        let env := M.alloc (| env |) in
        M.catch_return (|
          ltac:(M.monadic
            (M.read (|
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.lt (|
                                M.read (| gas_limit |),
                                M.read (|
                                  M.get_constant (|
                                    "revm_precompile::kzg_point_evaluation::GAS_COST"
                                  |)
                                |)
                              |)
                            |)) 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::precompile::PrecompileError::OutOfGas"
                                      []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    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.call_closure (|
                                  M.get_associated_function (|
                                    Ty.path "bytes::bytes::Bytes",
                                    "len",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::Deref",
                                        Ty.path "alloy_primitives::bytes_::Bytes",
                                        [],
                                        "deref",
                                        []
                                      |),
                                      [ M.read (| input |) ]
                                    |)
                                  ]
                                |),
                                Value.Integer IntegerKind.Usize 192
                              |)
                            |)) 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::precompile::PrecompileError::BlobInvalidInputLength"
                                      []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ versioned_hash :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::index::Index",
                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                      [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ],
                      "index",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::deref::Deref",
                          Ty.path "bytes::bytes::Bytes",
                          [],
                          "deref",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.path "alloy_primitives::bytes_::Bytes",
                              [],
                              "deref",
                              []
                            |),
                            [ M.read (| input |) ]
                          |)
                        ]
                      |);
                      Value.StructRecord
                        "core::ops::range::RangeTo"
                        [ ("end_", Value.Integer IntegerKind.Usize 32) ]
                    ]
                  |)
                |) in
              let~ commitment :=
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::index::Index",
                      Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                      [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] ],
                      "index",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::deref::Deref",
                          Ty.path "bytes::bytes::Bytes",
                          [],
                          "deref",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.path "alloy_primitives::bytes_::Bytes",
                              [],
                              "deref",
                              []
                            |),
                            [ M.read (| input |) ]
                          |)
                        ]
                      |);
                      Value.StructRecord
                        "core::ops::range::Range"
                        [
                          ("start", Value.Integer IntegerKind.Usize 96);
                          ("end_", Value.Integer IntegerKind.Usize 144)
                        ]
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "array")
                                    [ Value.Integer IntegerKind.Usize 32 ]
                                    [ Ty.path "u8" ],
                                  [
                                    Ty.apply
                                      (Ty.path "&")
                                      []
                                      [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                                  ],
                                  "ne",
                                  []
                                |),
                                [
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "revm_precompile::kzg_point_evaluation::kzg_to_versioned_hash",
                                        []
                                      |),
                                      [ M.read (| commitment |) ]
                                    |)
                                  |);
                                  versioned_hash
                                ]
                              |)
                            |)) 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::precompile::PrecompileError::BlobMismatchedVersion"
                                      []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              let~ commitment :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "revm_precompile::kzg_point_evaluation::as_bytes48", [] |),
                    [ M.read (| commitment |) ]
                  |)
                |) in
              let~ z :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "revm_precompile::kzg_point_evaluation::as_bytes32", [] |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::index::Index",
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] ],
                          "index",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.path "bytes::bytes::Bytes",
                              [],
                              "deref",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::deref::Deref",
                                  Ty.path "alloy_primitives::bytes_::Bytes",
                                  [],
                                  "deref",
                                  []
                                |),
                                [ M.read (| input |) ]
                              |)
                            ]
                          |);
                          Value.StructRecord
                            "core::ops::range::Range"
                            [
                              ("start", Value.Integer IntegerKind.Usize 32);
                              ("end_", Value.Integer IntegerKind.Usize 64)
                            ]
                        ]
                      |)
                    ]
                  |)
                |) in
              let~ y :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "revm_precompile::kzg_point_evaluation::as_bytes32", [] |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::index::Index",
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] ],
                          "index",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.path "bytes::bytes::Bytes",
                              [],
                              "deref",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::deref::Deref",
                                  Ty.path "alloy_primitives::bytes_::Bytes",
                                  [],
                                  "deref",
                                  []
                                |),
                                [ M.read (| input |) ]
                              |)
                            ]
                          |);
                          Value.StructRecord
                            "core::ops::range::Range"
                            [
                              ("start", Value.Integer IntegerKind.Usize 64);
                              ("end_", Value.Integer IntegerKind.Usize 96)
                            ]
                        ]
                      |)
                    ]
                  |)
                |) in
              let~ proof :=
                M.alloc (|
                  M.call_closure (|
                    M.get_function (| "revm_precompile::kzg_point_evaluation::as_bytes48", [] |),
                    [
                      M.call_closure (|
                        M.get_trait_method (|
                          "core::ops::index::Index",
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          [ Ty.apply (Ty.path "core::ops::range::Range") [] [ Ty.path "usize" ] ],
                          "index",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::deref::Deref",
                              Ty.path "bytes::bytes::Bytes",
                              [],
                              "deref",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::deref::Deref",
                                  Ty.path "alloy_primitives::bytes_::Bytes",
                                  [],
                                  "deref",
                                  []
                                |),
                                [ M.read (| input |) ]
                              |)
                            ]
                          |);
                          Value.StructRecord
                            "core::ops::range::Range"
                            [
                              ("start", Value.Integer IntegerKind.Usize 144);
                              ("end_", Value.Integer IntegerKind.Usize 192)
                            ]
                        ]
                      |)
                    ]
                  |)
                |) in
              let~ _ :=
                M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              UnOp.not (|
                                M.call_closure (|
                                  M.get_function (|
                                    "revm_precompile::kzg_point_evaluation::verify_kzg_proof",
                                    []
                                  |),
                                  [
                                    M.read (| commitment |);
                                    M.read (| z |);
                                    M.read (| y |);
                                    M.read (| proof |);
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.path
                                          "revm_primitives::kzg::env_settings::EnvKzgSettings",
                                        "get",
                                        []
                                      |),
                                      [
                                        M.SubPointer.get_struct_record_field (|
                                          M.SubPointer.get_struct_record_field (|
                                            M.read (| env |),
                                            "revm_primitives::env::Env",
                                            "cfg"
                                          |),
                                          "revm_primitives::env::CfgEnv",
                                          "kzg_settings"
                                        |)
                                      ]
                                    |)
                                  ]
                                |)
                              |)
                            |)) 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::precompile::PrecompileError::BlobVerifyKzgProofFailed"
                                      []
                                  ]
                              |)
                            |)
                          |)
                        |)));
                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                  ]
                |) in
              M.alloc (|
                Value.StructTuple
                  "core::result::Result::Ok"
                  [
                    Value.Tuple
                      [
                        M.read (|
                          M.get_constant (| "revm_precompile::kzg_point_evaluation::GAS_COST" |)
                        |);
                        M.call_closure (|
                          M.get_trait_method (|
                            "core::convert::Into",
                            Ty.apply
                              (Ty.path "&")
                              []
                              [
                                Ty.apply
                                  (Ty.path "array")
                                  [ Value.Integer IntegerKind.Usize 64 ]
                                  [ Ty.path "u8" ]
                              ],
                            [ Ty.path "alloy_primitives::bytes_::Bytes" ],
                            "into",
                            []
                          |),
                          [
                            M.read (|
                              M.get_constant (|
                                "revm_precompile::kzg_point_evaluation::RETURN_VALUE"
                              |)
                            |)
                          ]
                        |)
                      ]
                  ]
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_run : M.IsFunction "revm_precompile::kzg_point_evaluation::run" run.
  
  (*
  pub fn kzg_to_versioned_hash(commitment: &[u8]) -> [u8; 32] {
      let mut hash: [u8; 32] = Sha256::digest(commitment).into();
      hash[0] = VERSIONED_HASH_VERSION_KZG;
      hash
  }
  *)
  Definition kzg_to_versioned_hash (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ commitment ] =>
      ltac:(M.monadic
        (let commitment := M.alloc (| commitment |) in
        M.read (|
          let~ hash :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::convert::Into",
                  Ty.apply
                    (Ty.path "generic_array::GenericArray")
                    []
                    [
                      Ty.path "u8";
                      Ty.apply
                        (Ty.path "typenum::uint::UInt")
                        []
                        [
                          Ty.apply
                            (Ty.path "typenum::uint::UInt")
                            []
                            [
                              Ty.apply
                                (Ty.path "typenum::uint::UInt")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "typenum::uint::UInt")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "typenum::uint::UInt")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "typenum::uint::UInt")
                                            []
                                            [
                                              Ty.path "typenum::uint::UTerm";
                                              Ty.path "typenum::bit::B1"
                                            ];
                                          Ty.path "typenum::bit::B0"
                                        ];
                                      Ty.path "typenum::bit::B0"
                                    ];
                                  Ty.path "typenum::bit::B0"
                                ];
                              Ty.path "typenum::bit::B0"
                            ];
                          Ty.path "typenum::bit::B0"
                        ]
                    ],
                  [
                    Ty.apply
                      (Ty.path "array")
                      [ Value.Integer IntegerKind.Usize 32 ]
                      [ Ty.path "u8" ]
                  ],
                  "into",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "digest::digest::Digest",
                      Ty.apply
                        (Ty.path "digest::core_api::wrapper::CoreWrapper")
                        []
                        [
                          Ty.apply
                            (Ty.path "digest::core_api::ct_variable::CtVariableCoreWrapper")
                            []
                            [
                              Ty.path "sha2::core_api::Sha256VarCore";
                              Ty.apply
                                (Ty.path "typenum::uint::UInt")
                                []
                                [
                                  Ty.apply
                                    (Ty.path "typenum::uint::UInt")
                                    []
                                    [
                                      Ty.apply
                                        (Ty.path "typenum::uint::UInt")
                                        []
                                        [
                                          Ty.apply
                                            (Ty.path "typenum::uint::UInt")
                                            []
                                            [
                                              Ty.apply
                                                (Ty.path "typenum::uint::UInt")
                                                []
                                                [
                                                  Ty.apply
                                                    (Ty.path "typenum::uint::UInt")
                                                    []
                                                    [
                                                      Ty.path "typenum::uint::UTerm";
                                                      Ty.path "typenum::bit::B1"
                                                    ];
                                                  Ty.path "typenum::bit::B0"
                                                ];
                                              Ty.path "typenum::bit::B0"
                                            ];
                                          Ty.path "typenum::bit::B0"
                                        ];
                                      Ty.path "typenum::bit::B0"
                                    ];
                                  Ty.path "typenum::bit::B0"
                                ];
                              Ty.path "sha2::OidSha256"
                            ]
                        ],
                      [],
                      "digest",
                      [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ]
                      ]
                    |),
                    [ M.read (| commitment |) ]
                  |)
                ]
              |)
            |) in
          let~ _ :=
            M.write (|
              M.SubPointer.get_array_field (|
                hash,
                M.alloc (| Value.Integer IntegerKind.Usize 0 |)
              |),
              M.read (|
                M.get_constant (|
                  "revm_precompile::kzg_point_evaluation::VERSIONED_HASH_VERSION_KZG"
                |)
              |)
            |) in
          hash
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_kzg_to_versioned_hash :
    M.IsFunction
      "revm_precompile::kzg_point_evaluation::kzg_to_versioned_hash"
      kzg_to_versioned_hash.
  
  (*
  pub fn verify_kzg_proof(
      commitment: &Bytes48,
      z: &Bytes32,
      y: &Bytes32,
      proof: &Bytes48,
      kzg_settings: &KzgSettings,
  ) -> bool {
      KzgProof::verify_kzg_proof(commitment, z, y, proof, kzg_settings).unwrap_or(false)
  }
  *)
  Definition verify_kzg_proof (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ commitment; z; y; proof; kzg_settings ] =>
      ltac:(M.monadic
        (let commitment := M.alloc (| commitment |) in
        let z := M.alloc (| z |) in
        let y := M.alloc (| y |) in
        let proof := M.alloc (| proof |) in
        let kzg_settings := M.alloc (| kzg_settings |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "core::result::Result")
              []
              [ Ty.path "bool"; Ty.path "c_kzg::bindings::Error" ],
            "unwrap_or",
            []
          |),
          [
            M.call_closure (|
              M.get_associated_function (|
                Ty.path "c_kzg::bindings::KZGProof",
                "verify_kzg_proof",
                []
              |),
              [
                M.read (| commitment |);
                M.read (| z |);
                M.read (| y |);
                M.read (| proof |);
                M.read (| kzg_settings |)
              ]
            |);
            Value.Bool false
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_verify_kzg_proof :
    M.IsFunction "revm_precompile::kzg_point_evaluation::verify_kzg_proof" verify_kzg_proof.
  
  (*
  pub fn as_array<const N: usize>(bytes: &[u8]) -> &[u8; N] {
      bytes.try_into().expect("slice with incorrect length")
  }
  *)
  Definition as_array (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [ N ], [], [ bytes ] =>
      ltac:(M.monadic
        (let bytes := M.alloc (| bytes |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply
              (Ty.path "core::result::Result")
              []
              [
                Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ Ty.path "u8" ] ];
                Ty.path "core::array::TryFromSliceError"
              ],
            "expect",
            []
          |),
          [
            M.call_closure (|
              M.get_trait_method (|
                "core::convert::TryInto",
                Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "array") [ N ] [ Ty.path "u8" ] ] ],
                "try_into",
                []
              |),
              [ M.read (| bytes |) ]
            |);
            M.read (| Value.String "slice with incorrect length" |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_as_array : M.IsFunction "revm_precompile::kzg_point_evaluation::as_array" as_array.
  
  (*
  pub fn as_bytes32(bytes: &[u8]) -> &Bytes32 {
      // SAFETY: `#[repr(C)] Bytes32([u8; 32])`
      unsafe { &*as_array::<32>(bytes).as_ptr().cast() }
  }
  *)
  Definition as_bytes32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ bytes ] =>
      ltac:(M.monadic
        (let bytes := M.alloc (| bytes |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
            "cast",
            [ Ty.path "c_kzg::bindings::Bytes32" ]
          |),
          [
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                "as_ptr",
                []
              |),
              [
                M.call_closure (|
                  M.get_function (| "revm_precompile::kzg_point_evaluation::as_array", [] |),
                  [ M.read (| bytes |) ]
                |)
              ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_as_bytes32 :
    M.IsFunction "revm_precompile::kzg_point_evaluation::as_bytes32" as_bytes32.
  
  (*
  pub fn as_bytes48(bytes: &[u8]) -> &Bytes48 {
      // SAFETY: `#[repr(C)] Bytes48([u8; 48])`
      unsafe { &*as_array::<48>(bytes).as_ptr().cast() }
  }
  *)
  Definition as_bytes48 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ bytes ] =>
      ltac:(M.monadic
        (let bytes := M.alloc (| bytes |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.apply (Ty.path "*const") [] [ Ty.path "u8" ],
            "cast",
            [ Ty.path "c_kzg::bindings::Bytes48" ]
          |),
          [
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                "as_ptr",
                []
              |),
              [
                M.call_closure (|
                  M.get_function (| "revm_precompile::kzg_point_evaluation::as_array", [] |),
                  [ M.read (| bytes |) ]
                |)
              ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_as_bytes48 :
    M.IsFunction "revm_precompile::kzg_point_evaluation::as_bytes48" as_bytes48.
End kzg_point_evaluation.
