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

Module hash.
  Definition value_SHA256 : Value.t :=
    M.run
      ltac:(M.monadic
        (M.alloc (|
          Value.StructTuple
            "revm_precompile::PrecompileWithAddress"
            [
              M.call_closure (|
                M.get_function (| "revm_precompile::u64_to_address", [] |),
                [ Value.Integer IntegerKind.U64 2 ]
              |);
              Value.StructTuple
                "revm_primitives::precompile::Precompile::Standard"
                [
                  (* ReifyFnPointer *)
                  M.pointer_coercion (M.get_function (| "revm_precompile::hash::sha256_run", [] |))
                ]
            ]
        |))).
  
  Definition value_RIPEMD160 : Value.t :=
    M.run
      ltac:(M.monadic
        (M.alloc (|
          Value.StructTuple
            "revm_precompile::PrecompileWithAddress"
            [
              M.call_closure (|
                M.get_function (| "revm_precompile::u64_to_address", [] |),
                [ Value.Integer IntegerKind.U64 3 ]
              |);
              Value.StructTuple
                "revm_primitives::precompile::Precompile::Standard"
                [
                  (* ReifyFnPointer *)
                  M.pointer_coercion
                    (M.get_function (| "revm_precompile::hash::ripemd160_run", [] |))
                ]
            ]
        |))).
  
  (*
  pub fn sha256_run(input: &Bytes, gas_limit: u64) -> PrecompileResult {
      let cost = calc_linear_cost_u32(input.len(), 60, 12);
      if cost > gas_limit {
          Err(Error::OutOfGas)
      } else {
          let output = sha2::Sha256::digest(input);
          Ok((cost, output.to_vec().into()))
      }
  }
  *)
  Definition sha256_run (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ input; gas_limit ] =>
      ltac:(M.monadic
        (let input := M.alloc (| input |) in
        let gas_limit := M.alloc (| gas_limit |) in
        M.read (|
          let~ cost :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "revm_precompile::calc_linear_cost_u32", [] |),
                [
                  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.U64 60;
                  Value.Integer IntegerKind.U64 12
                ]
              |)
            |) in
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.use
                      (M.alloc (| BinOp.gt (| M.read (| cost |), M.read (| gas_limit |) |) |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Err"
                      [
                        Value.StructTuple
                          "revm_primitives::precompile::PrecompileError::OutOfGas"
                          []
                      ]
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let~ output :=
                    M.alloc (|
                      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.path "alloy_primitives::bytes_::Bytes" ]
                          ]
                        |),
                        [ M.read (| input |) ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Ok"
                      [
                        Value.Tuple
                          [
                            M.read (| cost |);
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::convert::Into",
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                                [ Ty.path "alloy_primitives::bytes_::Bytes" ],
                                "into",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "to_vec",
                                    []
                                  |),
                                  [
                                    M.call_closure (|
                                      M.get_trait_method (|
                                        "core::ops::deref::Deref",
                                        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"
                                              ]
                                          ],
                                        [],
                                        "deref",
                                        []
                                      |),
                                      [ output ]
                                    |)
                                  ]
                                |)
                              ]
                            |)
                          ]
                      ]
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_sha256_run : M.IsFunction "revm_precompile::hash::sha256_run" sha256_run.
  
  (*
  pub fn ripemd160_run(input: &Bytes, gas_limit: u64) -> PrecompileResult {
      let gas_used = calc_linear_cost_u32(input.len(), 600, 120);
      if gas_used > gas_limit {
          Err(Error::OutOfGas)
      } else {
          let mut hasher = ripemd::Ripemd160::new();
          hasher.update(input);
  
          let mut output = [0u8; 32];
          hasher.finalize_into((&mut output[12..]).into());
          Ok((gas_used, output.to_vec().into()))
      }
  }
  *)
  Definition ripemd160_run (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ input; gas_limit ] =>
      ltac:(M.monadic
        (let input := M.alloc (| input |) in
        let gas_limit := M.alloc (| gas_limit |) in
        M.read (|
          let~ gas_used :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "revm_precompile::calc_linear_cost_u32", [] |),
                [
                  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.U64 600;
                  Value.Integer IntegerKind.U64 120
                ]
              |)
            |) in
          M.match_operator (|
            M.alloc (| Value.Tuple [] |),
            [
              fun γ =>
                ltac:(M.monadic
                  (let γ :=
                    M.use
                      (M.alloc (|
                        BinOp.gt (| M.read (| gas_used |), M.read (| gas_limit |) |)
                      |)) in
                  let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Err"
                      [
                        Value.StructTuple
                          "revm_primitives::precompile::PrecompileError::OutOfGas"
                          []
                      ]
                  |)));
              fun γ =>
                ltac:(M.monadic
                  (let~ hasher :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "digest::digest::Digest",
                          Ty.apply
                            (Ty.path "digest::core_api::wrapper::CoreWrapper")
                            []
                            [ Ty.path "ripemd::Ripemd160Core" ],
                          [],
                          "new",
                          []
                        |),
                        []
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "digest::digest::Digest",
                          Ty.apply
                            (Ty.path "digest::core_api::wrapper::CoreWrapper")
                            []
                            [ Ty.path "ripemd::Ripemd160Core" ],
                          [],
                          "update",
                          [ Ty.apply (Ty.path "&") [] [ Ty.path "alloy_primitives::bytes_::Bytes" ]
                          ]
                        |),
                        [ hasher; M.read (| input |) ]
                      |)
                    |) in
                  let~ output :=
                    M.alloc (|
                      repeat (|
                        Value.Integer IntegerKind.U8 0,
                        Value.Integer IntegerKind.Usize 32
                      |)
                    |) in
                  let~ _ :=
                    M.alloc (|
                      M.call_closure (|
                        M.get_trait_method (|
                          "digest::digest::Digest",
                          Ty.apply
                            (Ty.path "digest::core_api::wrapper::CoreWrapper")
                            []
                            [ Ty.path "ripemd::Ripemd160Core" ],
                          [],
                          "finalize_into",
                          []
                        |),
                        [
                          M.read (| hasher |);
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::convert::Into",
                              Ty.apply
                                (Ty.path "&mut")
                                []
                                [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ] ],
                              [
                                Ty.apply
                                  (Ty.path "&mut")
                                  []
                                  [
                                    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.path "typenum::uint::UTerm";
                                                            Ty.path "typenum::bit::B1"
                                                          ];
                                                        Ty.path "typenum::bit::B0"
                                                      ];
                                                    Ty.path "typenum::bit::B1"
                                                  ];
                                                Ty.path "typenum::bit::B0"
                                              ];
                                            Ty.path "typenum::bit::B0"
                                          ]
                                      ]
                                  ]
                              ],
                              "into",
                              []
                            |),
                            [
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::index::IndexMut",
                                  Ty.apply
                                    (Ty.path "array")
                                    [ Value.Integer IntegerKind.Usize 32 ]
                                    [ Ty.path "u8" ],
                                  [
                                    Ty.apply
                                      (Ty.path "core::ops::range::RangeFrom")
                                      []
                                      [ Ty.path "usize" ]
                                  ],
                                  "index_mut",
                                  []
                                |),
                                [
                                  output;
                                  Value.StructRecord
                                    "core::ops::range::RangeFrom"
                                    [ ("start", Value.Integer IntegerKind.Usize 12) ]
                                ]
                              |)
                            ]
                          |)
                        ]
                      |)
                    |) in
                  M.alloc (|
                    Value.StructTuple
                      "core::result::Result::Ok"
                      [
                        Value.Tuple
                          [
                            M.read (| gas_used |);
                            M.call_closure (|
                              M.get_trait_method (|
                                "core::convert::Into",
                                Ty.apply
                                  (Ty.path "alloc::vec::Vec")
                                  []
                                  [ Ty.path "u8"; Ty.path "alloc::alloc::Global" ],
                                [ Ty.path "alloy_primitives::bytes_::Bytes" ],
                                "into",
                                []
                              |),
                              [
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                    "to_vec",
                                    []
                                  |),
                                  [ output ]
                                |)
                              ]
                            |)
                          ]
                      ]
                  |)))
            ]
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_ripemd160_run : M.IsFunction "revm_precompile::hash::ripemd160_run" ripemd160_run.
End hash.
