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

Module utilities.
  Definition value_KECCAK_EMPTY : Value.t :=
    M.run
      ltac:(M.monadic
        (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_primitives::utilities::KECCAK_EMPTY::RES" |) |) ]
          |)
        |))).
  
  (*
  pub fn calc_excess_blob_gas(parent_excess_blob_gas: u64, parent_blob_gas_used: u64) -> u64 {
      (parent_excess_blob_gas + parent_blob_gas_used).saturating_sub(TARGET_BLOB_GAS_PER_BLOCK)
  }
  *)
  Definition calc_excess_blob_gas (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ parent_excess_blob_gas; parent_blob_gas_used ] =>
      ltac:(M.monadic
        (let parent_excess_blob_gas := M.alloc (| parent_excess_blob_gas |) in
        let parent_blob_gas_used := M.alloc (| parent_blob_gas_used |) in
        M.call_closure (|
          M.get_associated_function (| Ty.path "u64", "saturating_sub", [] |),
          [
            BinOp.Wrap.add (|
              M.read (| parent_excess_blob_gas |),
              M.read (| parent_blob_gas_used |)
            |);
            M.read (|
              M.get_constant (| "revm_primitives::constants::TARGET_BLOB_GAS_PER_BLOCK" |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_calc_excess_blob_gas :
    M.IsFunction "revm_primitives::utilities::calc_excess_blob_gas" calc_excess_blob_gas.
  
  (*
  pub fn calc_blob_gasprice(excess_blob_gas: u64) -> u128 {
      fake_exponential(
          MIN_BLOB_GASPRICE,
          excess_blob_gas,
          BLOB_GASPRICE_UPDATE_FRACTION,
      )
  }
  *)
  Definition calc_blob_gasprice (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ excess_blob_gas ] =>
      ltac:(M.monadic
        (let excess_blob_gas := M.alloc (| excess_blob_gas |) in
        M.call_closure (|
          M.get_function (| "revm_primitives::utilities::fake_exponential", [] |),
          [
            M.read (| M.get_constant (| "revm_primitives::constants::MIN_BLOB_GASPRICE" |) |);
            M.read (| excess_blob_gas |);
            M.read (|
              M.get_constant (| "revm_primitives::constants::BLOB_GASPRICE_UPDATE_FRACTION" |)
            |)
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_calc_blob_gasprice :
    M.IsFunction "revm_primitives::utilities::calc_blob_gasprice" calc_blob_gasprice.
  
  (*
  pub fn fake_exponential(factor: u64, numerator: u64, denominator: u64) -> u128 {
      assert_ne!(denominator, 0, "attempt to divide by zero");
      let factor = factor as u128;
      let numerator = numerator as u128;
      let denominator = denominator as u128;
  
      let mut i = 1;
      let mut output = 0;
      let mut numerator_accum = factor * denominator;
      while numerator_accum > 0 {
          output += numerator_accum;
  
          // Denominator is asserted as not zero at the start of the function.
          numerator_accum = (numerator_accum * numerator) / (denominator * i);
          i += 1;
      }
      output / denominator
  }
  *)
  Definition fake_exponential (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ factor; numerator; denominator ] =>
      ltac:(M.monadic
        (let factor := M.alloc (| factor |) in
        let numerator := M.alloc (| numerator |) in
        let denominator := M.alloc (| denominator |) in
        M.read (|
          let~ _ :=
            M.match_operator (|
              M.alloc (|
                Value.Tuple [ denominator; M.alloc (| Value.Integer IntegerKind.U64 0 |) ]
              |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ0_0 := M.SubPointer.get_tuple_field (| γ, 0 |) in
                    let γ0_1 := M.SubPointer.get_tuple_field (| γ, 1 |) in
                    let left_val := M.copy (| γ0_0 |) in
                    let right_val := M.copy (| γ0_1 |) in
                    M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.eq (|
                                    M.read (| M.read (| left_val |) |),
                                    M.read (| M.read (| right_val |) |)
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.never_to_any (|
                                M.read (|
                                  let~ kind :=
                                    M.alloc (|
                                      Value.StructTuple "core::panicking::AssertKind::Ne" []
                                    |) in
                                  M.alloc (|
                                    M.call_closure (|
                                      M.get_function (|
                                        "core::panicking::assert_failed",
                                        [ Ty.path "u64"; Ty.path "u64" ]
                                      |),
                                      [
                                        M.read (| kind |);
                                        M.read (| left_val |);
                                        M.read (| right_val |);
                                        Value.StructTuple
                                          "core::option::Option::Some"
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "core::fmt::Arguments",
                                                "new_const",
                                                []
                                              |),
                                              [
                                                M.alloc (|
                                                  Value.Array
                                                    [
                                                      M.read (|
                                                        Value.String "attempt to divide by zero"
                                                      |)
                                                    ]
                                                |)
                                              ]
                                            |)
                                          ]
                                      ]
                                    |)
                                  |)
                                |)
                              |)
                            |)));
                        fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                      ]
                    |)))
              ]
            |) in
          let~ factor := M.alloc (| M.rust_cast (M.read (| factor |)) |) in
          let~ numerator := M.alloc (| M.rust_cast (M.read (| numerator |)) |) in
          let~ denominator := M.alloc (| M.rust_cast (M.read (| denominator |)) |) in
          let~ i := M.alloc (| Value.Integer IntegerKind.U128 1 |) in
          let~ output := M.alloc (| Value.Integer IntegerKind.U128 0 |) in
          let~ numerator_accum :=
            M.alloc (| BinOp.Wrap.mul (| M.read (| factor |), M.read (| denominator |) |) |) in
          let~ _ :=
            M.loop (|
              ltac:(M.monadic
                (M.match_operator (|
                  M.alloc (| Value.Tuple [] |),
                  [
                    fun γ =>
                      ltac:(M.monadic
                        (let γ :=
                          M.use
                            (M.alloc (|
                              BinOp.gt (|
                                M.read (| numerator_accum |),
                                Value.Integer IntegerKind.U128 0
                              |)
                            |)) in
                        let _ :=
                          M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                        let~ _ :=
                          let β := output in
                          M.write (|
                            β,
                            BinOp.Wrap.add (| M.read (| β |), M.read (| numerator_accum |) |)
                          |) in
                        let~ _ :=
                          M.write (|
                            numerator_accum,
                            BinOp.Wrap.div (|
                              BinOp.Wrap.mul (|
                                M.read (| numerator_accum |),
                                M.read (| numerator |)
                              |),
                              BinOp.Wrap.mul (| M.read (| denominator |), M.read (| i |) |)
                            |)
                          |) in
                        let~ _ :=
                          let β := i in
                          M.write (|
                            β,
                            BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.U128 1 |)
                          |) in
                        M.alloc (| Value.Tuple [] |)));
                    fun γ =>
                      ltac:(M.monadic
                        (M.alloc (|
                          M.never_to_any (|
                            M.read (|
                              let~ _ :=
                                M.alloc (| M.never_to_any (| M.read (| M.break (||) |) |) |) in
                              M.alloc (| Value.Tuple [] |)
                            |)
                          |)
                        |)))
                  ]
                |)))
            |) in
          M.alloc (| BinOp.Wrap.div (| M.read (| output |), M.read (| denominator |) |) |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_fake_exponential :
    M.IsFunction "revm_primitives::utilities::fake_exponential" fake_exponential.
End utilities.
