Skip to main content

⛽ Gas_limit_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Saturation_repr.

Definition decimals : int := 3.

Parameter fp_tag : Set.

Parameter integral_tag : Set.

Module S := Saturation_repr.

Definition scaling_factor : int := 1000.

Definition mul_scaling_factor : S.t := S.mul_safe_of_int_exn scaling_factor.

Module Arith.
  Definition t : Set := S.t.

  Definition fp : Set := t.

  Definition integral : Set := t.

  Definition mul_scaling_factor : S.t := mul_scaling_factor.

  Definition sub : S.t S.t S.t := S.sub.

  Definition add : S.t S.t S.t := S.add.

  Definition zero : S.t := S.zero.

  Definition min : S.t S.t S.t := S.min.

  Definition max : S.t S.t S.t := S.max.

  Definition compare : S.t S.t int := S.compare.

  Definition op_lt : S.t S.t bool := S.op_lt.

  Definition op_ltgt : S.t S.t bool := S.op_ltgt.

  Definition op_gt : S.t S.t bool := S.op_gt.

  Definition op_lteq : S.t S.t bool := S.op_lteq.

  Definition op_gteq : S.t S.t bool := S.op_gteq.

  Definition op_eq : S.t S.t bool := S.op_eq.

  Definition equal : S.t S.t bool := S.equal.

  Definition of_int_opt : int option S.t := S.of_int_opt.

  Definition fatally_saturated_int {A : Set} (i_value : int) : A :=
    Pervasives.failwith
      (Pervasives.op_caret (Pervasives.string_of_int i_value)
        " should not be saturated.").

  Definition fatally_saturated_z {A : Set} (z_value : Z.t) : A :=
    Pervasives.failwith
      (Pervasives.op_caret (Z.to_string z_value) " should not be saturated.").

  Definition integral_of_int_exn (i_value : int) : S.t :=
    match S.of_int_opt i_value with
    | Nonefatally_saturated_int i_value
    | Some i'
      let r_value := S.scale_fast mul_scaling_factor i' in
      if S.op_eq r_value S.saturated then
        fatally_saturated_int i_value
      else
        r_value
    end.

  Definition integral_exn (z_value : Z.t) : S.t :=
    let 'i_value := Z.to_int z_value in
    integral_of_int_exn i_value.

  Definition integral_to_z (i_value : integral) : Z.t :=
    S.to_z (S.ediv i_value mul_scaling_factor).

  Definition ceil (x_value : S.t) : S.t :=
    let r_value := S.erem x_value mul_scaling_factor in
    if op_eq r_value zero then
      x_value
    else
      add x_value (sub mul_scaling_factor r_value).

  Definition floor (x_value : S.t) : S.t :=
    sub x_value (S.erem x_value mul_scaling_factor).

  Definition fp_value {A : Set} (x_value : A) : A := x_value.

  Definition pp (fmtr : Format.formatter) (fp_value : S.t) : unit :=
    let q_value := S.to_int (S.ediv fp_value mul_scaling_factor) in
    let r_value := S.to_int (S.erem fp_value mul_scaling_factor) in
    if r_value =i 0 then
      Format.fprintf fmtr
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
            CamlinternalFormatBasics.No_padding
            CamlinternalFormatBasics.No_precision
            CamlinternalFormatBasics.End_of_format) "%d") q_value
    else
      Format.fprintf fmtr
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
            CamlinternalFormatBasics.No_padding
            CamlinternalFormatBasics.No_precision
            (CamlinternalFormatBasics.Char_literal "." % char
              (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                (CamlinternalFormatBasics.Arg_padding
                  CamlinternalFormatBasics.Zeros)
                CamlinternalFormatBasics.No_precision
                CamlinternalFormatBasics.End_of_format))) "%d.%0*d") q_value
        decimals r_value.

  Definition pp_integral : Format.formatter S.t unit := pp.

  Definition n_fp_encoding : Data_encoding.t fp := S.n_encoding.

  Definition z_fp_encoding : Data_encoding.t fp := S.z_encoding.

  Definition n_integral_encoding : Data_encoding.t integral :=
    Data_encoding.conv integral_to_z integral_exn None Data_encoding.n_value.

  Definition z_integral_encoding : Data_encoding.t integral :=
    Data_encoding.conv integral_to_z integral_exn None Data_encoding.z_value.

  Definition unsafe_fp (x_value : Z.t) : S.t :=
    match of_int_opt (Z.to_int x_value) with
    | Some int_valueint_value
    | Nonefatally_saturated_z x_value
    end.

  Definition sub_opt : S.t S.t option S.t := S.sub_opt.
End Arith.

Records for the constructor parameters
Module ConstructorRecords_t.
  Module t.
    Module Limited.
      Record record {remaining : Set} : Set := Build {
        remaining : remaining;
      }.
      Arguments record : clear implicits.
      Definition with_remaining {t_remaining} remaining
        (r : record t_remaining) :=
        Build t_remaining remaining.
    End Limited.
    Definition Limited_skeleton := Limited.record.
  End t.
End ConstructorRecords_t.
Import ConstructorRecords_t.

Reserved Notation "'t.Limited".

Inductive t : Set :=
| Unaccounted : t
| Limited : 't.Limited t

where "'t.Limited" := (t.Limited_skeleton Arith.fp).

Module t.
  Include ConstructorRecords_t.t.
  Definition Limited := 't.Limited.
End t.

Definition cost : Set := S.t.

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.union None
    [
      Data_encoding.case_value "Limited" None (Data_encoding.Tag 0)
        Arith.z_fp_encoding
        (fun (function_parameter : t) ⇒
          match function_parameter with
          | Limited {| t.Limited.remaining := remaining |} ⇒ Some remaining
          | _None
          end)
        (fun (remaining : Arith.fp) ⇒
          Limited {| t.Limited.remaining := remaining; |});
      Data_encoding.case_value "Unaccounted" None (Data_encoding.Tag 1)
        (Data_encoding.constant "unaccounted")
        (fun (function_parameter : t) ⇒
          match function_parameter with
          | UnaccountedSome tt
          | _None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Unaccounted)
    ].

Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
  match function_parameter with
  | Unaccounted
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "unaccounted"
          CamlinternalFormatBasics.End_of_format) "unaccounted")
  | Limited {| t.Limited.remaining := remaining |} ⇒
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.String_literal " units remaining"
            CamlinternalFormatBasics.End_of_format)) "%a units remaining")
      Arith.pp remaining
  end.

Definition cost_encoding : Data_encoding.t S.t := S.z_encoding.

Definition pp_cost (fmt : Format.formatter) (z_value : S.t) : unit :=
  S.pp fmt z_value.

Definition pp_cost_as_gas (fmt : Format.formatter) (z_value : S.t) : unit :=
  Format.pp_print_int fmt ((S.to_int (Arith.ceil z_value)) /i scaling_factor).

Definition allocation_weight : S.t :=
  S.mul_safe_exn (S.mul_fast mul_scaling_factor (S.mul_safe_of_int_exn 2)).

Definition step_weight : S.t := mul_scaling_factor.

Definition read_base_weight : S.t :=
  S.mul_safe_exn (S.mul_fast mul_scaling_factor (S.mul_safe_of_int_exn 100)).

Definition write_base_weight : S.t :=
  S.mul_safe_exn (S.mul_fast mul_scaling_factor (S.mul_safe_of_int_exn 160)).

Definition byte_read_weight : S.t :=
  S.mul_safe_exn (S.mul_fast mul_scaling_factor (S.mul_safe_of_int_exn 10)).

Definition byte_written_weight : S.t :=
  S.mul_safe_exn (S.mul_fast mul_scaling_factor (S.mul_safe_of_int_exn 15)).

Definition cost_to_milligas (cost : cost) : Arith.fp := cost.

Definition raw_consume (gas_counter : S.t) (cost : cost) : option S.t :=
  let gas := cost_to_milligas cost in
  Arith.sub_opt gas_counter gas.

Definition alloc_cost (n_value : S.t) : S.t :=
  S.scale_fast allocation_weight (S.add n_value (S.mul_safe_of_int_exn 1)).

Definition alloc_bytes_cost (n_value : int) : S.t :=
  alloc_cost (S.safe_int ((n_value +i 7) /i 8)).

Definition atomic_step_cost : S.t cost := S.may_saturate_value.

Definition step_cost (n_value : S.t) : S.t := S.scale_fast step_weight n_value.

Definition free : S.t := S.zero.

Definition cost_of_gas (gas : Arith.t) : cost := gas.

Definition fp_of_milligas_int (milligas : int) : Arith.fp :=
  Saturation_repr.safe_int milligas.

Definition read_bytes_cost (n_value : int) : S.t :=
  S.add read_base_weight (S.scale_fast byte_read_weight (S.safe_int n_value)).

Definition write_bytes_cost (n_value : int) : S.t :=
  S.add write_base_weight
    (S.scale_fast byte_written_weight (S.safe_int n_value)).

Definition op_plusat (x_value : S.t) (y_value : S.t) : S.t :=
  S.add x_value y_value.

Definition op_starat (x_value : S.t) (y_value : S.t) : S.t :=
  S.mul x_value y_value.

Definition alloc_mbytes_cost (n_value : int) : S.t :=
  op_plusat (alloc_cost (S.mul_safe_of_int_exn 12)) (alloc_bytes_cost n_value).

Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  Error_monad.register_error_kind Error_monad.Permanent "gas_limit_too_high"
    "Gas limit out of protocol hard bounds"
    "A transaction tried to exceed the hard limit on gas" None
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Gas_limit_too_high" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Gas_limit_too_high" unit tt).

Definition check_gas_limit
  (hard_gas_limit_per_operation : Arith.integral) (gas_limit : Arith.integral)
  : M? unit :=
  Error_monad.error_unless
    ((Arith.op_lteq gas_limit hard_gas_limit_per_operation) &&
    (Arith.op_gteq gas_limit Arith.zero))
    (Build_extensible "Gas_limit_too_high" unit tt).