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

Module utilities.
  (*
  pub fn right_pad_with_offset<const LEN: usize>(data: &[u8], offset: usize) -> Cow<'_, [u8; LEN]> {
      right_pad(data.get(offset..).unwrap_or_default())
  }
  *)
  Definition right_pad_with_offset (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [ LEN ], [], [ data; offset ] =>
      ltac:(M.monadic
        (let data := M.alloc (| data |) in
        let offset := M.alloc (| offset |) in
        M.call_closure (|
          M.get_function (| "revm_precompile::utilities::right_pad", [] |),
          [
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] ],
                "unwrap_or_default",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                    "get",
                    [ Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ] ]
                  |),
                  [
                    M.read (| data |);
                    Value.StructRecord
                      "core::ops::range::RangeFrom"
                      [ ("start", M.read (| offset |)) ]
                  ]
                |)
              ]
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_right_pad_with_offset :
    M.IsFunction "revm_precompile::utilities::right_pad_with_offset" right_pad_with_offset.
  
  (*
  pub fn right_pad_with_offset_vec(data: &[u8], offset: usize, len: usize) -> Cow<'_, [u8]> {
      right_pad_vec(data.get(offset..).unwrap_or_default(), len)
  }
  *)
  Definition right_pad_with_offset_vec (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ data; offset; len ] =>
      ltac:(M.monadic
        (let data := M.alloc (| data |) in
        let offset := M.alloc (| offset |) in
        let len := M.alloc (| len |) in
        M.call_closure (|
          M.get_function (| "revm_precompile::utilities::right_pad_vec", [] |),
          [
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "core::option::Option")
                  []
                  [ Ty.apply (Ty.path "&") [] [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ] ],
                "unwrap_or_default",
                []
              |),
              [
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                    "get",
                    [ Ty.apply (Ty.path "core::ops::range::RangeFrom") [] [ Ty.path "usize" ] ]
                  |),
                  [
                    M.read (| data |);
                    Value.StructRecord
                      "core::ops::range::RangeFrom"
                      [ ("start", M.read (| offset |)) ]
                  ]
                |)
              ]
            |);
            M.read (| len |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_right_pad_with_offset_vec :
    M.IsFunction "revm_precompile::utilities::right_pad_with_offset_vec" right_pad_with_offset_vec.
  
  (*
  pub fn right_pad<const LEN: usize>(data: &[u8]) -> Cow<'_, [u8; LEN]> {
      if let Some(data) = data.get(..LEN) {
          Cow::Borrowed(data.try_into().unwrap())
      } else {
          let mut padded = [0; LEN];
          padded[..data.len()].copy_from_slice(data);
          Cow::Owned(padded)
      }
  }
  *)
  Definition right_pad (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [ LEN ], [], [ data ] =>
      ltac:(M.monadic
        (let data := M.alloc (| data |) in
        M.read (|
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          "get",
                          [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ]
                        |),
                        [
                          M.read (| data |);
                          Value.StructRecord
                            "core::ops::range::RangeTo"
                            [
                              ("end_",
                                M.read (|
                                  M.get_constant (| "revm_precompile::utilities::right_pad::LEN" |)
                                |))
                            ]
                        ]
                      |)
                    |) in
                  let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::option::Option::Some", 0 |) in
                  let data := M.copy (| γ0_0 |) in
                  M.alloc (|
                    Value.StructTuple
                      "alloc::borrow::Cow::Borrowed"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.apply (Ty.path "array") [ LEN ] [ Ty.path "u8" ] ];
                                Ty.path "core::array::TryFromSliceError"
                              ],
                            "unwrap",
                            []
                          |),
                          [
                            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") [ LEN ] [ Ty.path "u8" ] ]
                                ],
                                "try_into",
                                []
                              |),
                              [ M.read (| data |) ]
                            |)
                          ]
                        |)
                      ]
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let~ padded := M.alloc (| repeat (| Value.Integer IntegerKind.U8 0, LEN |) |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          "copy_from_slice",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::index::IndexMut",
                              Ty.apply (Ty.path "array") [ LEN ] [ Ty.path "u8" ],
                              [
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeTo")
                                  []
                                  [ Ty.path "usize" ]
                              ],
                              "index_mut",
                              []
                            |),
                            [
                              padded;
                              Value.StructRecord
                                "core::ops::range::RangeTo"
                                [
                                  ("end_",
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| data |) ]
                                    |))
                                ]
                            ]
                          |);
                          M.read (| data |)
                        ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple "alloc::borrow::Cow::Owned" [ M.read (| padded |) ]
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_right_pad : M.IsFunction "revm_precompile::utilities::right_pad" right_pad.
  
  (*
  pub fn right_pad_vec(data: &[u8], len: usize) -> Cow<'_, [u8]> {
      if let Some(data) = data.get(..len) {
          Cow::Borrowed(data)
      } else {
          let mut padded = vec![0; len];
          padded[..data.len()].copy_from_slice(data);
          Cow::Owned(padded)
      }
  }
  *)
  Definition right_pad_vec (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ data; len ] =>
      ltac:(M.monadic
        (let data := M.alloc (| data |) in
        let len := M.alloc (| len |) in
        M.read (|
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          "get",
                          [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ]
                        |),
                        [
                          M.read (| data |);
                          Value.StructRecord
                            "core::ops::range::RangeTo"
                            [ ("end_", M.read (| len |)) ]
                        ]
                      |)
                    |) in
                  let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::option::Option::Some", 0 |) in
                  let data := M.copy (| γ0_0 |) in
                  M.alloc (|
                    Value.StructTuple "alloc::borrow::Cow::Borrowed" [ M.read (| data |) ]
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let~ padded :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "alloc::vec::from_elem", [ Ty.path "u8" ] |),
                        [ Value.Integer IntegerKind.U8 0; M.read (| len |) ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          "copy_from_slice",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::index::IndexMut",
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                              [
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeTo")
                                  []
                                  [ Ty.path "usize" ]
                              ],
                              "index_mut",
                              []
                            |),
                            [
                              padded;
                              Value.StructRecord
                                "core::ops::range::RangeTo"
                                [
                                  ("end_",
                                    M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                        "len",
                                        []
                                      |),
                                      [ M.read (| data |) ]
                                    |))
                                ]
                            ]
                          |);
                          M.read (| data |)
                        ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple "alloc::borrow::Cow::Owned" [ M.read (| padded |) ]
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_right_pad_vec :
    M.IsFunction "revm_precompile::utilities::right_pad_vec" right_pad_vec.
  
  (*
  pub fn left_pad<const LEN: usize>(data: &[u8]) -> Cow<'_, [u8; LEN]> {
      if let Some(data) = data.get(..LEN) {
          Cow::Borrowed(data.try_into().unwrap())
      } else {
          let mut padded = [0; LEN];
          padded[LEN - data.len()..].copy_from_slice(data);
          Cow::Owned(padded)
      }
  }
  *)
  Definition left_pad (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [ LEN ], [], [ data ] =>
      ltac:(M.monadic
        (let data := M.alloc (| data |) in
        M.read (|
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          "get",
                          [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ]
                        |),
                        [
                          M.read (| data |);
                          Value.StructRecord
                            "core::ops::range::RangeTo"
                            [
                              ("end_",
                                M.read (|
                                  M.get_constant (| "revm_precompile::utilities::left_pad::LEN" |)
                                |))
                            ]
                        ]
                      |)
                    |) in
                  let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::option::Option::Some", 0 |) in
                  let data := M.copy (| γ0_0 |) in
                  M.alloc (|
                    Value.StructTuple
                      "alloc::borrow::Cow::Borrowed"
                      [
                        M.call_closure (|
                          M.get_associated_function (|
                            Ty.apply
                              (Ty.path "core::result::Result")
                              []
                              [
                                Ty.apply
                                  (Ty.path "&")
                                  []
                                  [ Ty.apply (Ty.path "array") [ LEN ] [ Ty.path "u8" ] ];
                                Ty.path "core::array::TryFromSliceError"
                              ],
                            "unwrap",
                            []
                          |),
                          [
                            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") [ LEN ] [ Ty.path "u8" ] ]
                                ],
                                "try_into",
                                []
                              |),
                              [ M.read (| data |) ]
                            |)
                          ]
                        |)
                      ]
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let~ padded := M.alloc (| repeat (| Value.Integer IntegerKind.U8 0, LEN |) |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          "copy_from_slice",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::index::IndexMut",
                              Ty.apply (Ty.path "array") [ LEN ] [ Ty.path "u8" ],
                              [
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeFrom")
                                  []
                                  [ Ty.path "usize" ]
                              ],
                              "index_mut",
                              []
                            |),
                            [
                              padded;
                              Value.StructRecord
                                "core::ops::range::RangeFrom"
                                [
                                  ("start",
                                    BinOp.Wrap.sub (|
                                      M.read (|
                                        M.get_constant (|
                                          "revm_precompile::utilities::left_pad::LEN"
                                        |)
                                      |),
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                          "len",
                                          []
                                        |),
                                        [ M.read (| data |) ]
                                      |)
                                    |))
                                ]
                            ]
                          |);
                          M.read (| data |)
                        ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple "alloc::borrow::Cow::Owned" [ M.read (| padded |) ]
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_left_pad : M.IsFunction "revm_precompile::utilities::left_pad" left_pad.
  
  (*
  pub fn left_pad_vec(data: &[u8], len: usize) -> Cow<'_, [u8]> {
      if let Some(data) = data.get(..len) {
          Cow::Borrowed(data)
      } else {
          let mut padded = vec![0; len];
          padded[len - data.len()..].copy_from_slice(data);
          Cow::Owned(padded)
      }
  }
  *)
  Definition left_pad_vec (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ data; len ] =>
      ltac:(M.monadic
        (let data := M.alloc (| data |) in
        let len := M.alloc (| len |) in
        M.read (|
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          "get",
                          [ Ty.apply (Ty.path "core::ops::range::RangeTo") [] [ Ty.path "usize" ] ]
                        |),
                        [
                          M.read (| data |);
                          Value.StructRecord
                            "core::ops::range::RangeTo"
                            [ ("end_", M.read (| len |)) ]
                        ]
                      |)
                    |) in
                  let γ0_0 :=
                    M.SubPointer.get_struct_tuple_field (| γ, "core::option::Option::Some", 0 |) in
                  let data := M.copy (| γ0_0 |) in
                  M.alloc (|
                    Value.StructTuple "alloc::borrow::Cow::Borrowed" [ M.read (| data |) ]
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let~ padded :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_function (| "alloc::vec::from_elem", [ Ty.path "u8" ] |),
                        [ Value.Integer IntegerKind.U8 0; M.read (| len |) ]
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                          "copy_from_slice",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::ops::index::IndexMut",
                              Ty.apply
                                (Ty.path "alloc::vec::Vec")
                                []
                                [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                              [
                                Ty.apply
                                  (Ty.path "core::ops::range::RangeFrom")
                                  []
                                  [ Ty.path "usize" ]
                              ],
                              "index_mut",
                              []
                            |),
                            [
                              padded;
                              Value.StructRecord
                                "core::ops::range::RangeFrom"
                                [
                                  ("start",
                                    BinOp.Wrap.sub (|
                                      M.read (| len |),
                                      M.call_closure (|
                                        M.get_associated_function (|
                                          Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                          "len",
                                          []
                                        |),
                                        [ M.read (| data |) ]
                                      |)
                                    |))
                                ]
                            ]
                          |);
                          M.read (| data |)
                        ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple "alloc::borrow::Cow::Owned" [ M.read (| padded |) ]
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_left_pad_vec :
    M.IsFunction "revm_precompile::utilities::left_pad_vec" left_pad_vec.
  
  (*
  pub const fn bool_to_bytes32(value: bool) -> Bytes {
      Bytes::from_static(&bool_to_b256(value).0)
  }
  *)
  Definition bool_to_bytes32 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ value ] =>
      ltac:(M.monadic
        (let value := M.alloc (| value |) in
        M.call_closure (|
          M.get_associated_function (|
            Ty.path "alloy_primitives::bytes_::Bytes",
            "from_static",
            []
          |),
          [
            M.SubPointer.get_struct_tuple_field (|
              M.call_closure (|
                M.get_function (| "revm_precompile::utilities::bool_to_b256", [] |),
                [ M.read (| value |) ]
              |),
              "alloy_primitives::bits::fixed::FixedBytes",
              0
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_bool_to_bytes32 :
    M.IsFunction "revm_precompile::utilities::bool_to_bytes32" bool_to_bytes32.
  
  (*
  pub const fn bool_to_b256(value: bool) -> &'static B256 {
      const TRUE: &B256 = &b256!("0000000000000000000000000000000000000000000000000000000000000001");
      const FALSE: &B256 = &b256!("0000000000000000000000000000000000000000000000000000000000000000");
      if value {
          TRUE
      } else {
          FALSE
      }
  }
  *)
  Definition bool_to_b256 (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ value ] =>
      ltac:(M.monadic
        (let value := M.alloc (| value |) in
        M.read (|
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ := M.use value in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.get_constant (| "revm_precompile::utilities::bool_to_b256::TRUE" |)));
              fun γ =>
                ltac:(M.monadic
                  (M.get_constant (| "revm_precompile::utilities::bool_to_b256::FALSE" |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_bool_to_b256 :
    M.IsFunction "revm_precompile::utilities::bool_to_b256" bool_to_b256.
  
  Module bool_to_b256.
    Definition value_TRUE : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                    [ Value.Integer IntegerKind.Usize 32 ]
                    [],
                  "new",
                  []
                |),
                [
                  M.read (|
                    M.get_constant (| "revm_precompile::utilities::bool_to_b256::TRUE::RES" |)
                  |)
                ]
              |)
            |)
          |))).
    
    Definition value_FALSE : Value.t :=
      M.run
        ltac:(M.monadic
          (M.alloc (|
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "alloy_primitives::bits::fixed::FixedBytes")
                    [ Value.Integer IntegerKind.Usize 32 ]
                    [],
                  "new",
                  []
                |),
                [
                  M.read (|
                    M.get_constant (| "revm_precompile::utilities::bool_to_b256::FALSE::RES" |)
                  |)
                ]
              |)
            |)
          |))).
  End bool_to_b256.
End utilities.
