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

Module modexp.
  Definition value_BYZANTIUM : 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 5 ]
              |);
              Value.StructTuple
                "revm_primitives::precompile::Precompile::Standard"
                [
                  (* ReifyFnPointer *)
                  M.pointer_coercion
                    (M.get_function (| "revm_precompile::modexp::byzantium_run", [] |))
                ]
            ]
        |))).
  
  Definition value_BERLIN : 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 5 ]
              |);
              Value.StructTuple
                "revm_primitives::precompile::Precompile::Standard"
                [
                  (* ReifyFnPointer *)
                  M.pointer_coercion
                    (M.get_function (| "revm_precompile::modexp::berlin_run", [] |))
                ]
            ]
        |))).
  
  (*
  pub fn byzantium_run(input: &Bytes, gas_limit: u64) -> PrecompileResult {
      run_inner(input, gas_limit, 0, |a, b, c, d| {
          byzantium_gas_calc(a, b, c, d)
      })
  }
  *)
  Definition byzantium_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.call_closure (|
          M.get_function (|
            "revm_precompile::modexp::run_inner",
            [
              Ty.function
                [
                  Ty.tuple
                    [
                      Ty.path "u64";
                      Ty.path "u64";
                      Ty.path "u64";
                      Ty.apply
                        (Ty.path "&")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            []
                        ]
                    ]
                ]
                (Ty.path "u64")
            ]
          |),
          [
            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 |) ]
                |)
              ]
            |);
            M.read (| gas_limit |);
            Value.Integer IntegerKind.U64 0;
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0; α1; α2; α3 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let a := M.copy (| γ |) in
                              M.match_operator (|
                                M.alloc (| α1 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let b := M.copy (| γ |) in
                                      M.match_operator (|
                                        M.alloc (| α2 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let c := M.copy (| γ |) in
                                              M.match_operator (|
                                                M.alloc (| α3 |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let d := M.copy (| γ |) in
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "revm_precompile::modexp::byzantium_gas_calc",
                                                          []
                                                        |),
                                                        [
                                                          M.read (| a |);
                                                          M.read (| b |);
                                                          M.read (| c |);
                                                          M.read (| d |)
                                                        ]
                                                      |)))
                                                ]
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_byzantium_run :
    M.IsFunction "revm_precompile::modexp::byzantium_run" byzantium_run.
  
  (*
  pub fn berlin_run(input: &Bytes, gas_limit: u64) -> PrecompileResult {
      run_inner(input, gas_limit, 200, |a, b, c, d| {
          berlin_gas_calc(a, b, c, d)
      })
  }
  *)
  Definition berlin_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.call_closure (|
          M.get_function (|
            "revm_precompile::modexp::run_inner",
            [
              Ty.function
                [
                  Ty.tuple
                    [
                      Ty.path "u64";
                      Ty.path "u64";
                      Ty.path "u64";
                      Ty.apply
                        (Ty.path "&")
                        []
                        [
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            []
                        ]
                    ]
                ]
                (Ty.path "u64")
            ]
          |),
          [
            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 |) ]
                |)
              ]
            |);
            M.read (| gas_limit |);
            Value.Integer IntegerKind.U64 200;
            M.closure
              (fun γ =>
                ltac:(M.monadic
                  match γ with
                  | [ α0; α1; α2; α3 ] =>
                    ltac:(M.monadic
                      (M.match_operator (|
                        M.alloc (| α0 |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let a := M.copy (| γ |) in
                              M.match_operator (|
                                M.alloc (| α1 |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let b := M.copy (| γ |) in
                                      M.match_operator (|
                                        M.alloc (| α2 |),
                                        [
                                          fun γ =>
                                            ltac:(M.monadic
                                              (let c := M.copy (| γ |) in
                                              M.match_operator (|
                                                M.alloc (| α3 |),
                                                [
                                                  fun γ =>
                                                    ltac:(M.monadic
                                                      (let d := M.copy (| γ |) in
                                                      M.call_closure (|
                                                        M.get_function (|
                                                          "revm_precompile::modexp::berlin_gas_calc",
                                                          []
                                                        |),
                                                        [
                                                          M.read (| a |);
                                                          M.read (| b |);
                                                          M.read (| c |);
                                                          M.read (| d |)
                                                        ]
                                                      |)))
                                                ]
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)))
                        ]
                      |)))
                  | _ => M.impossible "wrong number of arguments"
                  end))
          ]
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_berlin_run : M.IsFunction "revm_precompile::modexp::berlin_run" berlin_run.
  
  (*
  pub fn calculate_iteration_count(exp_length: u64, exp_highp: &U256) -> u64 {
      let mut iteration_count: u64 = 0;
  
      if exp_length <= 32 && *exp_highp == U256::ZERO {
          iteration_count = 0;
      } else if exp_length <= 32 {
          iteration_count = exp_highp.bit_len() as u64 - 1;
      } else if exp_length > 32 {
          iteration_count = (8u64.saturating_mul(exp_length - 32))
              .saturating_add(max(1, exp_highp.bit_len() as u64) - 1);
      }
  
      max(iteration_count, 1)
  }
  *)
  Definition calculate_iteration_count (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ exp_length; exp_highp ] =>
      ltac:(M.monadic
        (let exp_length := M.alloc (| exp_length |) in
        let exp_highp := M.alloc (| exp_highp |) in
        M.read (|
          let~ iteration_count := M.alloc (| Value.Integer IntegerKind.U64 0 |) in
          let~ _ :=
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          LogicalOp.and (|
                            BinOp.le (|
                              M.read (| exp_length |),
                              Value.Integer IntegerKind.U64 32
                            |),
                            ltac:(M.monadic
                              (M.call_closure (|
                                M.get_trait_method (|
                                  "core::cmp::PartialEq",
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    [],
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      []
                                  ],
                                  "eq",
                                  []
                                |),
                                [ M.read (| exp_highp |); M.get_constant (| "ruint::ZERO" |) ]
                              |)))
                          |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    let~ _ := M.write (| iteration_count, Value.Integer IntegerKind.U64 0 |) in
                    M.alloc (| Value.Tuple [] |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.le (|
                                    M.read (| exp_length |),
                                    Value.Integer IntegerKind.U64 32
                                  |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            let~ _ :=
                              M.write (|
                                iteration_count,
                                BinOp.Wrap.sub (|
                                  M.rust_cast
                                    (M.call_closure (|
                                      M.get_associated_function (|
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          [],
                                        "bit_len",
                                        []
                                      |),
                                      [ M.read (| exp_highp |) ]
                                    |)),
                                  Value.Integer IntegerKind.U64 1
                                |)
                              |) in
                            M.alloc (| Value.Tuple [] |)));
                        fun γ =>
                          ltac:(M.monadic
                            (M.match_operator (|
                              M.alloc (| Value.Tuple [] |),
                              [
                                fun γ =>
                                  ltac:(M.monadic
                                    (let γ :=
                                      M.use
                                        (M.alloc (|
                                          BinOp.gt (|
                                            M.read (| exp_length |),
                                            Value.Integer IntegerKind.U64 32
                                          |)
                                        |)) in
                                    let _ :=
                                      M.is_constant_or_break_match (|
                                        M.read (| γ |),
                                        Value.Bool true
                                      |) in
                                    let~ _ :=
                                      M.write (|
                                        iteration_count,
                                        M.call_closure (|
                                          M.get_associated_function (|
                                            Ty.path "u64",
                                            "saturating_add",
                                            []
                                          |),
                                          [
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.path "u64",
                                                "saturating_mul",
                                                []
                                              |),
                                              [
                                                Value.Integer IntegerKind.U64 8;
                                                BinOp.Wrap.sub (|
                                                  M.read (| exp_length |),
                                                  Value.Integer IntegerKind.U64 32
                                                |)
                                              ]
                                            |);
                                            BinOp.Wrap.sub (|
                                              M.call_closure (|
                                                M.get_function (|
                                                  "core::cmp::max",
                                                  [ Ty.path "u64" ]
                                                |),
                                                [
                                                  Value.Integer IntegerKind.U64 1;
                                                  M.rust_cast
                                                    (M.call_closure (|
                                                      M.get_associated_function (|
                                                        Ty.apply
                                                          (Ty.path "ruint::Uint")
                                                          [
                                                            Value.Integer IntegerKind.Usize 256;
                                                            Value.Integer IntegerKind.Usize 4
                                                          ]
                                                          [],
                                                        "bit_len",
                                                        []
                                                      |),
                                                      [ M.read (| exp_highp |) ]
                                                    |))
                                                ]
                                              |),
                                              Value.Integer IntegerKind.U64 1
                                            |)
                                          ]
                                        |)
                                      |) in
                                    M.alloc (| Value.Tuple [] |)));
                                fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                              ]
                            |)))
                      ]
                    |)))
              ]
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_function (| "core::cmp::max", [ Ty.path "u64" ] |),
              [ M.read (| iteration_count |); Value.Integer IntegerKind.U64 1 ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_calculate_iteration_count :
    M.IsFunction "revm_precompile::modexp::calculate_iteration_count" calculate_iteration_count.
  
  (*
  pub fn run_inner<F>(input: &[u8], gas_limit: u64, min_gas: u64, calc_gas: F) -> PrecompileResult
  where
      F: FnOnce(u64, u64, u64, &U256) -> u64,
  {
      // If there is no minimum gas, return error.
      if min_gas > gas_limit {
          return Err(Error::OutOfGas);
      }
  
      // The format of input is:
      // <length_of_BASE> <length_of_EXPONENT> <length_of_MODULUS> <BASE> <EXPONENT> <MODULUS>
      // Where every length is a 32-byte left-padded integer representing the number of bytes
      // to be taken up by the next value
      const HEADER_LENGTH: usize = 96;
  
      // Extract the header.
      let base_len = U256::from_be_bytes(right_pad_with_offset::<32>(input, 0).into_owned());
      let exp_len = U256::from_be_bytes(right_pad_with_offset::<32>(input, 32).into_owned());
      let mod_len = U256::from_be_bytes(right_pad_with_offset::<32>(input, 64).into_owned());
  
      // cast base and modulus to usize, it does not make sense to handle larger values
      let Ok(base_len) = usize::try_from(base_len) else {
          return Err(Error::ModexpBaseOverflow);
      };
      let Ok(mod_len) = usize::try_from(mod_len) else {
          return Err(Error::ModexpModOverflow);
      };
  
      // Handle a special case when both the base and mod length are zero.
      if base_len == 0 && mod_len == 0 {
          return Ok((min_gas, Bytes::new()));
      }
  
      // Cast exponent length to usize, since it does not make sense to handle larger values.
      let Ok(exp_len) = usize::try_from(exp_len) else {
          return Err(Error::ModexpModOverflow);
      };
  
      // Used to extract ADJUSTED_EXPONENT_LENGTH.
      let exp_highp_len = min(exp_len, 32);
  
      // Throw away the header data as we already extracted lengths.
      let input = input.get(HEADER_LENGTH..).unwrap_or_default();
  
      let exp_highp = {
          // get right padded bytes so if data.len is less then exp_len we will get right padded zeroes.
          let right_padded_highp = right_pad_with_offset::<32>(input, base_len);
          // If exp_len is less then 32 bytes get only exp_len bytes and do left padding.
          let out = left_pad::<32>(&right_padded_highp[..exp_highp_len]);
          U256::from_be_bytes(out.into_owned())
      };
  
      // Check if we have enough gas.
      let gas_cost = calc_gas(base_len as u64, exp_len as u64, mod_len as u64, &exp_highp);
      if gas_cost > gas_limit {
          return Err(Error::OutOfGas);
      }
  
      // Padding is needed if the input does not contain all 3 values.
      let input_len = base_len.saturating_add(exp_len).saturating_add(mod_len);
      let input = right_pad_vec(input, input_len);
      let (base, input) = input.split_at(base_len);
      let (exponent, modulus) = input.split_at(exp_len);
      debug_assert_eq!(modulus.len(), mod_len);
  
      // Call the modexp.
      let output = modexp(base, exponent, modulus);
  
      // left pad the result to modulus length. bytes will always by less or equal to modulus length.
      Ok((gas_cost, left_pad_vec(&output, mod_len).into_owned().into()))
  }
  *)
  Definition run_inner (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [ F ], [ input; gas_limit; min_gas; calc_gas ] =>
      ltac:(M.monadic
        (let input := M.alloc (| input |) in
        let gas_limit := M.alloc (| gas_limit |) in
        let min_gas := M.alloc (| min_gas |) in
        let calc_gas := M.alloc (| calc_gas |) 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.gt (| M.read (| min_gas |), M.read (| gas_limit |) |)
                            |)) 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~ base_len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [],
                      "from_be_bytes",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::borrow::Cow")
                            []
                            [
                              Ty.apply
                                (Ty.path "array")
                                [ Value.Integer IntegerKind.Usize 32 ]
                                [ Ty.path "u8" ]
                            ],
                          "into_owned",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_function (|
                              "revm_precompile::utilities::right_pad_with_offset",
                              []
                            |),
                            [ M.read (| input |); Value.Integer IntegerKind.Usize 0 ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              let~ exp_len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [],
                      "from_be_bytes",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::borrow::Cow")
                            []
                            [
                              Ty.apply
                                (Ty.path "array")
                                [ Value.Integer IntegerKind.Usize 32 ]
                                [ Ty.path "u8" ]
                            ],
                          "into_owned",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_function (|
                              "revm_precompile::utilities::right_pad_with_offset",
                              []
                            |),
                            [ M.read (| input |); Value.Integer IntegerKind.Usize 32 ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              let~ mod_len :=
                M.alloc (|
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [],
                      "from_be_bytes",
                      []
                    |),
                    [
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "alloc::borrow::Cow")
                            []
                            [
                              Ty.apply
                                (Ty.path "array")
                                [ Value.Integer IntegerKind.Usize 32 ]
                                [ Ty.path "u8" ]
                            ],
                          "into_owned",
                          []
                        |),
                        [
                          M.call_closure (|
                            M.get_function (|
                              "revm_precompile::utilities::right_pad_with_offset",
                              []
                            |),
                            [ M.read (| input |); Value.Integer IntegerKind.Usize 64 ]
                          |)
                        ]
                      |)
                    ]
                  |)
                |) in
              M.match_operator (|
                M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::convert::TryFrom",
                      Ty.path "usize",
                      [
                        Ty.apply
                          (Ty.path "ruint::Uint")
                          [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                          []
                      ],
                      "try_from",
                      []
                    |),
                    [ M.read (| base_len |) ]
                  |)
                |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ0_0 :=
                        M.SubPointer.get_struct_tuple_field (|
                          γ,
                          "core::result::Result::Ok",
                          0
                        |) in
                      let base_len := M.copy (| γ0_0 |) in
                      M.match_operator (|
                        M.alloc (|
                          M.call_closure (|
                            M.get_trait_method (|
                              "core::convert::TryFrom",
                              Ty.path "usize",
                              [
                                Ty.apply
                                  (Ty.path "ruint::Uint")
                                  [
                                    Value.Integer IntegerKind.Usize 256;
                                    Value.Integer IntegerKind.Usize 4
                                  ]
                                  []
                              ],
                              "try_from",
                              []
                            |),
                            [ M.read (| mod_len |) ]
                          |)
                        |),
                        [
                          fun γ =>
                            ltac:(M.monadic
                              (let γ0_0 :=
                                M.SubPointer.get_struct_tuple_field (|
                                  γ,
                                  "core::result::Result::Ok",
                                  0
                                |) in
                              let mod_len := M.copy (| γ0_0 |) in
                              let~ _ :=
                                M.match_operator (|
                                  M.alloc (| Value.Tuple [] |),
                                  [
                                    fun γ =>
                                      ltac:(M.monadic
                                        (let γ :=
                                          M.use
                                            (M.alloc (|
                                              LogicalOp.and (|
                                                BinOp.eq (|
                                                  M.read (| base_len |),
                                                  Value.Integer IntegerKind.Usize 0
                                                |),
                                                ltac:(M.monadic
                                                  (BinOp.eq (|
                                                    M.read (| mod_len |),
                                                    Value.Integer IntegerKind.Usize 0
                                                  |)))
                                              |)
                                            |)) 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::Ok"
                                                  [
                                                    Value.Tuple
                                                      [
                                                        M.read (| min_gas |);
                                                        M.call_closure (|
                                                          M.get_associated_function (|
                                                            Ty.path
                                                              "alloy_primitives::bytes_::Bytes",
                                                            "new",
                                                            []
                                                          |),
                                                          []
                                                        |)
                                                      ]
                                                  ]
                                              |)
                                            |)
                                          |)
                                        |)));
                                    fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                                  ]
                                |) in
                              M.match_operator (|
                                M.alloc (|
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::convert::TryFrom",
                                      Ty.path "usize",
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          []
                                      ],
                                      "try_from",
                                      []
                                    |),
                                    [ M.read (| exp_len |) ]
                                  |)
                                |),
                                [
                                  fun γ =>
                                    ltac:(M.monadic
                                      (let γ0_0 :=
                                        M.SubPointer.get_struct_tuple_field (|
                                          γ,
                                          "core::result::Result::Ok",
                                          0
                                        |) in
                                      let exp_len := M.copy (| γ0_0 |) in
                                      let~ exp_highp_len :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "core::cmp::min",
                                              [ Ty.path "usize" ]
                                            |),
                                            [
                                              M.read (| exp_len |);
                                              Value.Integer IntegerKind.Usize 32
                                            ]
                                          |)
                                        |) in
                                      let~ input :=
                                        M.alloc (|
                                          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 (| input |);
                                                  Value.StructRecord
                                                    "core::ops::range::RangeFrom"
                                                    [
                                                      ("start",
                                                        M.read (|
                                                          M.get_constant (|
                                                            "revm_precompile::modexp::run_inner::HEADER_LENGTH"
                                                          |)
                                                        |))
                                                    ]
                                                ]
                                              |)
                                            ]
                                          |)
                                        |) in
                                      let~ exp_highp :=
                                        M.copy (|
                                          let~ right_padded_highp :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_function (|
                                                  "revm_precompile::utilities::right_pad_with_offset",
                                                  []
                                                |),
                                                [ M.read (| input |); M.read (| base_len |) ]
                                              |)
                                            |) in
                                          let~ out :=
                                            M.alloc (|
                                              M.call_closure (|
                                                M.get_function (|
                                                  "revm_precompile::utilities::left_pad",
                                                  []
                                                |),
                                                [
                                                  M.call_closure (|
                                                    M.get_trait_method (|
                                                      "core::ops::index::Index",
                                                      Ty.apply
                                                        (Ty.path "array")
                                                        [ Value.Integer IntegerKind.Usize 32 ]
                                                        [ 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.apply
                                                            (Ty.path "alloc::borrow::Cow")
                                                            []
                                                            [
                                                              Ty.apply
                                                                (Ty.path "array")
                                                                [ Value.Integer IntegerKind.Usize 32
                                                                ]
                                                                [ Ty.path "u8" ]
                                                            ],
                                                          [],
                                                          "deref",
                                                          []
                                                        |),
                                                        [ right_padded_highp ]
                                                      |);
                                                      Value.StructRecord
                                                        "core::ops::range::RangeTo"
                                                        [ ("end_", M.read (| exp_highp_len |)) ]
                                                    ]
                                                  |)
                                                ]
                                              |)
                                            |) in
                                          M.alloc (|
                                            M.call_closure (|
                                              M.get_associated_function (|
                                                Ty.apply
                                                  (Ty.path "ruint::Uint")
                                                  [
                                                    Value.Integer IntegerKind.Usize 256;
                                                    Value.Integer IntegerKind.Usize 4
                                                  ]
                                                  [],
                                                "from_be_bytes",
                                                []
                                              |),
                                              [
                                                M.call_closure (|
                                                  M.get_associated_function (|
                                                    Ty.apply
                                                      (Ty.path "alloc::borrow::Cow")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "array")
                                                          [ Value.Integer IntegerKind.Usize 32 ]
                                                          [ Ty.path "u8" ]
                                                      ],
                                                    "into_owned",
                                                    []
                                                  |),
                                                  [ M.read (| out |) ]
                                                |)
                                              ]
                                            |)
                                          |)
                                        |) in
                                      let~ gas_cost :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_trait_method (|
                                              "core::ops::function::FnOnce",
                                              F,
                                              [
                                                Ty.tuple
                                                  [
                                                    Ty.path "u64";
                                                    Ty.path "u64";
                                                    Ty.path "u64";
                                                    Ty.apply
                                                      (Ty.path "&")
                                                      []
                                                      [
                                                        Ty.apply
                                                          (Ty.path "ruint::Uint")
                                                          [
                                                            Value.Integer IntegerKind.Usize 256;
                                                            Value.Integer IntegerKind.Usize 4
                                                          ]
                                                          []
                                                      ]
                                                  ]
                                              ],
                                              "call_once",
                                              []
                                            |),
                                            [
                                              M.read (| calc_gas |);
                                              Value.Tuple
                                                [
                                                  M.rust_cast (M.read (| base_len |));
                                                  M.rust_cast (M.read (| exp_len |));
                                                  M.rust_cast (M.read (| mod_len |));
                                                  exp_highp
                                                ]
                                            ]
                                          |)
                                        |) in
                                      let~ _ :=
                                        M.match_operator (|
                                          M.alloc (| Value.Tuple [] |),
                                          [
                                            fun γ =>
                                              ltac:(M.monadic
                                                (let γ :=
                                                  M.use
                                                    (M.alloc (|
                                                      BinOp.gt (|
                                                        M.read (| gas_cost |),
                                                        M.read (| gas_limit |)
                                                      |)
                                                    |)) 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~ input_len :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.path "usize",
                                              "saturating_add",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_associated_function (|
                                                  Ty.path "usize",
                                                  "saturating_add",
                                                  []
                                                |),
                                                [ M.read (| base_len |); M.read (| exp_len |) ]
                                              |);
                                              M.read (| mod_len |)
                                            ]
                                          |)
                                        |) in
                                      let~ input :=
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_function (|
                                              "revm_precompile::utilities::right_pad_vec",
                                              []
                                            |),
                                            [ M.read (| input |); M.read (| input_len |) ]
                                          |)
                                        |) in
                                      M.match_operator (|
                                        M.alloc (|
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ],
                                              "split_at",
                                              []
                                            |),
                                            [
                                              M.call_closure (|
                                                M.get_trait_method (|
                                                  "core::ops::deref::Deref",
                                                  Ty.apply
                                                    (Ty.path "alloc::borrow::Cow")
                                                    []
                                                    [ Ty.apply (Ty.path "slice") [] [ Ty.path "u8" ]
                                                    ],
                                                  [],
                                                  "deref",
                                                  []
                                                |),
                                                [ input ]
                                              |);
                                              M.read (| base_len |)
                                            ]
                                          |)
                                        |),
                                        [
                                          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 base := M.copy (| γ0_0 |) in
                                              let input := M.copy (| γ0_1 |) in
                                              M.match_operator (|
                                                M.alloc (|
                                                  M.call_closure (|
                                                    M.get_associated_function (|
                                                      Ty.apply
                                                        (Ty.path "slice")
                                                        []
                                                        [ Ty.path "u8" ],
                                                      "split_at",
                                                      []
                                                    |),
                                                    [ M.read (| input |); M.read (| exp_len |) ]
                                                  |)
                                                |),
                                                [
                                                  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 exponent := M.copy (| γ0_0 |) in
                                                      let modulus := M.copy (| γ0_1 |) in
                                                      let~ _ :=
                                                        M.match_operator (|
                                                          M.alloc (| Value.Tuple [] |),
                                                          [
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (let γ :=
                                                                  M.use
                                                                    (M.alloc (|
                                                                      Value.Bool true
                                                                    |)) in
                                                                let _ :=
                                                                  M.is_constant_or_break_match (|
                                                                    M.read (| γ |),
                                                                    Value.Bool true
                                                                  |) in
                                                                let~ _ :=
                                                                  M.match_operator (|
                                                                    M.alloc (|
                                                                      Value.Tuple
                                                                        [
                                                                          M.alloc (|
                                                                            M.call_closure (|
                                                                              M.get_associated_function (|
                                                                                Ty.apply
                                                                                  (Ty.path "slice")
                                                                                  []
                                                                                  [ Ty.path "u8" ],
                                                                                "len",
                                                                                []
                                                                              |),
                                                                              [ M.read (| modulus |)
                                                                              ]
                                                                            |)
                                                                          |);
                                                                          mod_len
                                                                        ]
                                                                    |),
                                                                    [
                                                                      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 (|
                                                                                        UnOp.not (|
                                                                                          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::Eq"
                                                                                              []
                                                                                          |) in
                                                                                        M.alloc (|
                                                                                          M.call_closure (|
                                                                                            M.get_function (|
                                                                                              "core::panicking::assert_failed",
                                                                                              [
                                                                                                Ty.path
                                                                                                  "usize";
                                                                                                Ty.path
                                                                                                  "usize"
                                                                                              ]
                                                                                            |),
                                                                                            [
                                                                                              M.read (|
                                                                                                kind
                                                                                              |);
                                                                                              M.read (|
                                                                                                left_val
                                                                                              |);
                                                                                              M.read (|
                                                                                                right_val
                                                                                              |);
                                                                                              Value.StructTuple
                                                                                                "core::option::Option::None"
                                                                                                []
                                                                                            ]
                                                                                          |)
                                                                                        |)
                                                                                      |)
                                                                                    |)
                                                                                  |)));
                                                                              fun γ =>
                                                                                ltac:(M.monadic
                                                                                  (M.alloc (|
                                                                                    Value.Tuple []
                                                                                  |)))
                                                                            ]
                                                                          |)))
                                                                    ]
                                                                  |) in
                                                                M.alloc (| Value.Tuple [] |)));
                                                            fun γ =>
                                                              ltac:(M.monadic
                                                                (M.alloc (| Value.Tuple [] |)))
                                                          ]
                                                        |) in
                                                      let~ output :=
                                                        M.alloc (|
                                                          M.call_closure (|
                                                            M.get_function (|
                                                              "aurora_engine_modexp::modexp",
                                                              []
                                                            |),
                                                            [
                                                              M.read (| base |);
                                                              M.read (| exponent |);
                                                              M.read (| modulus |)
                                                            ]
                                                          |)
                                                        |) in
                                                      M.alloc (|
                                                        Value.StructTuple
                                                          "core::result::Result::Ok"
                                                          [
                                                            Value.Tuple
                                                              [
                                                                M.read (| gas_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
                                                                            "alloc::borrow::Cow")
                                                                          []
                                                                          [
                                                                            Ty.apply
                                                                              (Ty.path "slice")
                                                                              []
                                                                              [ Ty.path "u8" ]
                                                                          ],
                                                                        "into_owned",
                                                                        []
                                                                      |),
                                                                      [
                                                                        M.call_closure (|
                                                                          M.get_function (|
                                                                            "revm_precompile::utilities::left_pad_vec",
                                                                            []
                                                                          |),
                                                                          [
                                                                            M.call_closure (|
                                                                              M.get_trait_method (|
                                                                                "core::ops::deref::Deref",
                                                                                Ty.apply
                                                                                  (Ty.path
                                                                                    "alloc::vec::Vec")
                                                                                  []
                                                                                  [
                                                                                    Ty.path "u8";
                                                                                    Ty.path
                                                                                      "alloc::alloc::Global"
                                                                                  ],
                                                                                [],
                                                                                "deref",
                                                                                []
                                                                              |),
                                                                              [ output ]
                                                                            |);
                                                                            M.read (| mod_len |)
                                                                          ]
                                                                        |)
                                                                      ]
                                                                    |)
                                                                  ]
                                                                |)
                                                              ]
                                                          ]
                                                      |)))
                                                ]
                                              |)))
                                        ]
                                      |)))
                                ]
                              |)))
                        ]
                      |)))
                ]
              |)
            |)))
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_run_inner : M.IsFunction "revm_precompile::modexp::run_inner" run_inner.
  
  Module run_inner.
    Definition value_HEADER_LENGTH : Value.t :=
      M.run ltac:(M.monadic (M.alloc (| Value.Integer IntegerKind.Usize 96 |))).
  End run_inner.
  
  (*
  pub fn byzantium_gas_calc(base_len: u64, exp_len: u64, mod_len: u64, exp_highp: &U256) -> u64 {
      // output of this function is bounded by 2^128
      fn mul_complexity(x: u64) -> U256 {
          if x <= 64 {
              U256::from(x * x)
          } else if x <= 1_024 {
              U256::from(x * x / 4 + 96 * x - 3_072)
          } else {
              // up-cast to avoid overflow
              let x = U256::from(x);
              let x_sq = x * x; // x < 2^64 => x*x < 2^128 < 2^256 (no overflow)
              x_sq / U256::from(16) + U256::from(480) * x - U256::from(199_680)
          }
      }
  
      let mul = mul_complexity(core::cmp::max(mod_len, base_len));
      let iter_count = U256::from(calculate_iteration_count(exp_len, exp_highp));
      // mul * iter_count bounded by 2^195 < 2^256 (no overflow)
      let gas = (mul * iter_count) / U256::from(20);
      gas.saturating_to()
  }
  *)
  Definition byzantium_gas_calc (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ base_len; exp_len; mod_len; exp_highp ] =>
      ltac:(M.monadic
        (let base_len := M.alloc (| base_len |) in
        let exp_len := M.alloc (| exp_len |) in
        let mod_len := M.alloc (| mod_len |) in
        let exp_highp := M.alloc (| exp_highp |) in
        M.read (|
          let~ mul :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "revm_precompile::modexp::byzantium_gas_calc.mul_complexity",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_function (| "core::cmp::max", [ Ty.path "u64" ] |),
                    [ M.read (| mod_len |); M.read (| base_len |) ]
                  |)
                ]
              |)
            |) in
          let~ iter_count :=
            M.alloc (|
              M.call_closure (|
                M.get_associated_function (|
                  Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    [],
                  "from",
                  [ Ty.path "u64" ]
                |),
                [
                  M.call_closure (|
                    M.get_function (| "revm_precompile::modexp::calculate_iteration_count", [] |),
                    [ M.read (| exp_len |); M.read (| exp_highp |) ]
                  |)
                ]
              |)
            |) in
          let~ gas :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::arith::Div",
                  Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    [],
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      []
                  ],
                  "div",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::arith::Mul",
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [],
                      [
                        Ty.apply
                          (Ty.path "ruint::Uint")
                          [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                          []
                      ],
                      "mul",
                      []
                    |),
                    [ M.read (| mul |); M.read (| iter_count |) ]
                  |);
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [],
                      "from",
                      [ Ty.path "i32" ]
                    |),
                    [ Value.Integer IntegerKind.I32 20 ]
                  |)
                ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_associated_function (|
                Ty.apply
                  (Ty.path "ruint::Uint")
                  [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                  [],
                "saturating_to",
                [ Ty.path "u64" ]
              |),
              [ gas ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_byzantium_gas_calc :
    M.IsFunction "revm_precompile::modexp::byzantium_gas_calc" byzantium_gas_calc.
  
  Module byzantium_gas_calc.
    (*
        fn mul_complexity(x: u64) -> U256 {
            if x <= 64 {
                U256::from(x * x)
            } else if x <= 1_024 {
                U256::from(x * x / 4 + 96 * x - 3_072)
            } else {
                // up-cast to avoid overflow
                let x = U256::from(x);
                let x_sq = x * x; // x < 2^64 => x*x < 2^128 < 2^256 (no overflow)
                x_sq / U256::from(16) + U256::from(480) * x - U256::from(199_680)
            }
        }
    *)
    Definition mul_complexity (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
      match ε, τ, α with
      | [], [], [ x ] =>
        ltac:(M.monadic
          (let x := M.alloc (| x |) in
          M.read (|
            M.match_operator (|
              M.alloc (| Value.Tuple [] |),
              [
                fun γ =>
                  ltac:(M.monadic
                    (let γ :=
                      M.use
                        (M.alloc (|
                          BinOp.le (| M.read (| x |), Value.Integer IntegerKind.U64 64 |)
                        |)) in
                    let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                    M.alloc (|
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [],
                          "from",
                          [ Ty.path "u64" ]
                        |),
                        [ BinOp.Wrap.mul (| M.read (| x |), M.read (| x |) |) ]
                      |)
                    |)));
                fun γ =>
                  ltac:(M.monadic
                    (M.match_operator (|
                      M.alloc (| Value.Tuple [] |),
                      [
                        fun γ =>
                          ltac:(M.monadic
                            (let γ :=
                              M.use
                                (M.alloc (|
                                  BinOp.le (| M.read (| x |), Value.Integer IntegerKind.U64 1024 |)
                                |)) in
                            let _ :=
                              M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_associated_function (|
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    [],
                                  "from",
                                  [ Ty.path "u64" ]
                                |),
                                [
                                  BinOp.Wrap.sub (|
                                    BinOp.Wrap.add (|
                                      BinOp.Wrap.div (|
                                        BinOp.Wrap.mul (| M.read (| x |), M.read (| x |) |),
                                        Value.Integer IntegerKind.U64 4
                                      |),
                                      BinOp.Wrap.mul (|
                                        Value.Integer IntegerKind.U64 96,
                                        M.read (| x |)
                                      |)
                                    |),
                                    Value.Integer IntegerKind.U64 3072
                                  |)
                                ]
                              |)
                            |)));
                        fun γ =>
                          ltac:(M.monadic
                            (let~ x :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_associated_function (|
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [],
                                    "from",
                                    [ Ty.path "u64" ]
                                  |),
                                  [ M.read (| x |) ]
                                |)
                              |) in
                            let~ x_sq :=
                              M.alloc (|
                                M.call_closure (|
                                  M.get_trait_method (|
                                    "core::ops::arith::Mul",
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      [],
                                    [
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        []
                                    ],
                                    "mul",
                                    []
                                  |),
                                  [ M.read (| x |); M.read (| x |) ]
                                |)
                              |) in
                            M.alloc (|
                              M.call_closure (|
                                M.get_trait_method (|
                                  "core::ops::arith::Sub",
                                  Ty.apply
                                    (Ty.path "ruint::Uint")
                                    [
                                      Value.Integer IntegerKind.Usize 256;
                                      Value.Integer IntegerKind.Usize 4
                                    ]
                                    [],
                                  [
                                    Ty.apply
                                      (Ty.path "ruint::Uint")
                                      [
                                        Value.Integer IntegerKind.Usize 256;
                                        Value.Integer IntegerKind.Usize 4
                                      ]
                                      []
                                  ],
                                  "sub",
                                  []
                                |),
                                [
                                  M.call_closure (|
                                    M.get_trait_method (|
                                      "core::ops::arith::Add",
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        [],
                                      [
                                        Ty.apply
                                          (Ty.path "ruint::Uint")
                                          [
                                            Value.Integer IntegerKind.Usize 256;
                                            Value.Integer IntegerKind.Usize 4
                                          ]
                                          []
                                      ],
                                      "add",
                                      []
                                    |),
                                    [
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::arith::Div",
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            [],
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              []
                                          ],
                                          "div",
                                          []
                                        |),
                                        [
                                          M.read (| x_sq |);
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                [],
                                              "from",
                                              [ Ty.path "i32" ]
                                            |),
                                            [ Value.Integer IntegerKind.I32 16 ]
                                          |)
                                        ]
                                      |);
                                      M.call_closure (|
                                        M.get_trait_method (|
                                          "core::ops::arith::Mul",
                                          Ty.apply
                                            (Ty.path "ruint::Uint")
                                            [
                                              Value.Integer IntegerKind.Usize 256;
                                              Value.Integer IntegerKind.Usize 4
                                            ]
                                            [],
                                          [
                                            Ty.apply
                                              (Ty.path "ruint::Uint")
                                              [
                                                Value.Integer IntegerKind.Usize 256;
                                                Value.Integer IntegerKind.Usize 4
                                              ]
                                              []
                                          ],
                                          "mul",
                                          []
                                        |),
                                        [
                                          M.call_closure (|
                                            M.get_associated_function (|
                                              Ty.apply
                                                (Ty.path "ruint::Uint")
                                                [
                                                  Value.Integer IntegerKind.Usize 256;
                                                  Value.Integer IntegerKind.Usize 4
                                                ]
                                                [],
                                              "from",
                                              [ Ty.path "i32" ]
                                            |),
                                            [ Value.Integer IntegerKind.I32 480 ]
                                          |);
                                          M.read (| x |)
                                        ]
                                      |)
                                    ]
                                  |);
                                  M.call_closure (|
                                    M.get_associated_function (|
                                      Ty.apply
                                        (Ty.path "ruint::Uint")
                                        [
                                          Value.Integer IntegerKind.Usize 256;
                                          Value.Integer IntegerKind.Usize 4
                                        ]
                                        [],
                                      "from",
                                      [ Ty.path "i32" ]
                                    |),
                                    [ Value.Integer IntegerKind.I32 199680 ]
                                  |)
                                ]
                              |)
                            |)))
                      ]
                    |)))
              ]
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_mul_complexity :
      M.IsFunction "revm_precompile::modexp::byzantium_gas_calc::mul_complexity" mul_complexity.
  End byzantium_gas_calc.
  
  (*
  pub fn berlin_gas_calc(
      base_length: u64,
      exp_length: u64,
      mod_length: u64,
      exp_highp: &U256,
  ) -> u64 {
      fn calculate_multiplication_complexity(base_length: u64, mod_length: u64) -> U256 {
          let max_length = max(base_length, mod_length);
          let mut words = max_length / 8;
          if max_length % 8 > 0 {
              words += 1;
          }
          let words = U256::from(words);
          words * words
      }
  
      let multiplication_complexity = calculate_multiplication_complexity(base_length, mod_length);
      let iteration_count = calculate_iteration_count(exp_length, exp_highp);
      let gas = (multiplication_complexity * U256::from(iteration_count)) / U256::from(3);
      max(200, gas.saturating_to())
  }
  *)
  Definition berlin_gas_calc (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
    match ε, τ, α with
    | [], [], [ base_length; exp_length; mod_length; exp_highp ] =>
      ltac:(M.monadic
        (let base_length := M.alloc (| base_length |) in
        let exp_length := M.alloc (| exp_length |) in
        let mod_length := M.alloc (| mod_length |) in
        let exp_highp := M.alloc (| exp_highp |) in
        M.read (|
          let~ multiplication_complexity :=
            M.alloc (|
              M.call_closure (|
                M.get_function (|
                  "revm_precompile::modexp::berlin_gas_calc.calculate_multiplication_complexity",
                  []
                |),
                [ M.read (| base_length |); M.read (| mod_length |) ]
              |)
            |) in
          let~ iteration_count :=
            M.alloc (|
              M.call_closure (|
                M.get_function (| "revm_precompile::modexp::calculate_iteration_count", [] |),
                [ M.read (| exp_length |); M.read (| exp_highp |) ]
              |)
            |) in
          let~ gas :=
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::arith::Div",
                  Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    [],
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      []
                  ],
                  "div",
                  []
                |),
                [
                  M.call_closure (|
                    M.get_trait_method (|
                      "core::ops::arith::Mul",
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [],
                      [
                        Ty.apply
                          (Ty.path "ruint::Uint")
                          [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                          []
                      ],
                      "mul",
                      []
                    |),
                    [
                      M.read (| multiplication_complexity |);
                      M.call_closure (|
                        M.get_associated_function (|
                          Ty.apply
                            (Ty.path "ruint::Uint")
                            [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4
                            ]
                            [],
                          "from",
                          [ Ty.path "u64" ]
                        |),
                        [ M.read (| iteration_count |) ]
                      |)
                    ]
                  |);
                  M.call_closure (|
                    M.get_associated_function (|
                      Ty.apply
                        (Ty.path "ruint::Uint")
                        [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                        [],
                      "from",
                      [ Ty.path "i32" ]
                    |),
                    [ Value.Integer IntegerKind.I32 3 ]
                  |)
                ]
              |)
            |) in
          M.alloc (|
            M.call_closure (|
              M.get_function (| "core::cmp::max", [ Ty.path "u64" ] |),
              [
                Value.Integer IntegerKind.U64 200;
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [],
                    "saturating_to",
                    [ Ty.path "u64" ]
                  |),
                  [ gas ]
                |)
              ]
            |)
          |)
        |)))
    | _, _, _ => M.impossible "wrong number of arguments"
    end.
  
  Axiom Function_berlin_gas_calc :
    M.IsFunction "revm_precompile::modexp::berlin_gas_calc" berlin_gas_calc.
  
  Module berlin_gas_calc.
    (*
        fn calculate_multiplication_complexity(base_length: u64, mod_length: u64) -> U256 {
            let max_length = max(base_length, mod_length);
            let mut words = max_length / 8;
            if max_length % 8 > 0 {
                words += 1;
            }
            let words = U256::from(words);
            words * words
        }
    *)
    Definition calculate_multiplication_complexity
        (ε : list Value.t)
        (τ : list Ty.t)
        (α : list Value.t)
        : M :=
      match ε, τ, α with
      | [], [], [ base_length; mod_length ] =>
        ltac:(M.monadic
          (let base_length := M.alloc (| base_length |) in
          let mod_length := M.alloc (| mod_length |) in
          M.read (|
            let~ max_length :=
              M.alloc (|
                M.call_closure (|
                  M.get_function (| "core::cmp::max", [ Ty.path "u64" ] |),
                  [ M.read (| base_length |); M.read (| mod_length |) ]
                |)
              |) in
            let~ words :=
              M.alloc (|
                BinOp.Wrap.div (| M.read (| max_length |), Value.Integer IntegerKind.U64 8 |)
              |) in
            let~ _ :=
              M.match_operator (|
                M.alloc (| Value.Tuple [] |),
                [
                  fun γ =>
                    ltac:(M.monadic
                      (let γ :=
                        M.use
                          (M.alloc (|
                            BinOp.gt (|
                              BinOp.Wrap.rem (|
                                M.read (| max_length |),
                                Value.Integer IntegerKind.U64 8
                              |),
                              Value.Integer IntegerKind.U64 0
                            |)
                          |)) in
                      let _ := M.is_constant_or_break_match (| M.read (| γ |), Value.Bool true |) in
                      let~ _ :=
                        let β := words in
                        M.write (|
                          β,
                          BinOp.Wrap.add (| M.read (| β |), Value.Integer IntegerKind.U64 1 |)
                        |) in
                      M.alloc (| Value.Tuple [] |)));
                  fun γ => ltac:(M.monadic (M.alloc (| Value.Tuple [] |)))
                ]
              |) in
            let~ words :=
              M.alloc (|
                M.call_closure (|
                  M.get_associated_function (|
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      [],
                    "from",
                    [ Ty.path "u64" ]
                  |),
                  [ M.read (| words |) ]
                |)
              |) in
            M.alloc (|
              M.call_closure (|
                M.get_trait_method (|
                  "core::ops::arith::Mul",
                  Ty.apply
                    (Ty.path "ruint::Uint")
                    [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                    [],
                  [
                    Ty.apply
                      (Ty.path "ruint::Uint")
                      [ Value.Integer IntegerKind.Usize 256; Value.Integer IntegerKind.Usize 4 ]
                      []
                  ],
                  "mul",
                  []
                |),
                [ M.read (| words |); M.read (| words |) ]
              |)
            |)
          |)))
      | _, _, _ => M.impossible "wrong number of arguments"
      end.
    
    Axiom Function_calculate_multiplication_complexity :
      M.IsFunction
        "revm_precompile::modexp::berlin_gas_calc::calculate_multiplication_complexity"
        calculate_multiplication_complexity.
  End berlin_gas_calc.
End modexp.
