⛽ Gas_limit_repr.v
Translated 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
| None ⇒ fatally_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_value ⇒ int_value
| None ⇒ fatally_saturated_z x_value
end.
Definition sub_opt : S.t → S.t → option S.t := S.sub_opt.
End Arith.
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
| None ⇒ fatally_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_value ⇒ int_value
| None ⇒ fatally_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
| Unaccounted ⇒ Some 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).
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
| Unaccounted ⇒ Some 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).
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).