From d5f472d2e5dab630d8492d38e6aaba47310796d1 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Fri, 13 Nov 2020 13:21:31 +0100 Subject: [PATCH 01/23] Proto: Use saturated arithmetic in the cost model implementation Signed-off-by: Yann Regis-Gianas --- src/proto_alpha/lib_protocol/alpha_context.ml | 2 +- .../lib_protocol/alpha_context.mli | 12 +- .../lib_protocol/gas_limit_repr.ml | 78 ++- .../lib_protocol/gas_limit_repr.mli | 16 +- .../lib_protocol/michelson_v1_gas.ml | 516 ++++++++++-------- .../lib_protocol/michelson_v1_gas.mli | 6 +- .../lib_protocol/sapling_storage.ml | 8 +- .../lib_protocol/saturation_repr.ml | 4 + .../lib_protocol/saturation_repr.mli | 7 + .../lib_protocol/script_interpreter.ml | 13 +- src/proto_alpha/lib_protocol/script_repr.ml | 14 +- src/proto_alpha/lib_protocol/storage_costs.ml | 8 +- .../lib_protocol/test/test_gas_costs.ml | 17 +- .../lib_protocol/test/test_gas_levels.ml | 9 +- .../lib_protocol/test/test_gas_properties.ml | 11 +- .../lib_protocol/test/test_script_gas.ml | 11 +- 16 files changed, 408 insertions(+), 324 deletions(-) diff --git a/src/proto_alpha/lib_protocol/alpha_context.ml b/src/proto_alpha/lib_protocol/alpha_context.ml index f0fea8ae116c..a0e2c784b8df 100644 --- a/src/proto_alpha/lib_protocol/alpha_context.ml +++ b/src/proto_alpha/lib_protocol/alpha_context.ml @@ -190,7 +190,7 @@ module Big_map = struct let get_opt c m k = Storage.Big_map.Contents.find (c, m) k let exists c id = - Raw_context.consume_gas c (Gas_limit_repr.read_bytes_cost Z.zero) + Raw_context.consume_gas c (Gas_limit_repr.read_bytes_cost 0) >>?= fun c -> Storage.Big_map.Key_type.find c id >>=? fun kt -> diff --git a/src/proto_alpha/lib_protocol/alpha_context.mli b/src/proto_alpha/lib_protocol/alpha_context.mli index 46fa8608d026..fd13affaa020 100644 --- a/src/proto_alpha/lib_protocol/alpha_context.mli +++ b/src/proto_alpha/lib_protocol/alpha_context.mli @@ -189,21 +189,21 @@ module Gas : sig val free : cost - val atomic_step_cost : Z.t -> cost + val atomic_step_cost : 'a Saturation_repr.t -> cost - val step_cost : Z.t -> cost + val step_cost : 'a Saturation_repr.t -> cost - val alloc_cost : Z.t -> cost + val alloc_cost : 'a Saturation_repr.t -> cost val alloc_bytes_cost : int -> cost val alloc_mbytes_cost : int -> cost - val read_bytes_cost : Z.t -> cost + val read_bytes_cost : int -> cost - val write_bytes_cost : Z.t -> cost + val write_bytes_cost : int -> cost - val ( *@ ) : Z.t -> cost -> cost + val ( *@ ) : 'a Saturation_repr.t -> cost -> cost val ( +@ ) : cost -> cost -> cost diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.ml b/src/proto_alpha/lib_protocol/gas_limit_repr.ml index 64afdae25821..c51382460496 100644 --- a/src/proto_alpha/lib_protocol/gas_limit_repr.ml +++ b/src/proto_alpha/lib_protocol/gas_limit_repr.ml @@ -29,7 +29,22 @@ type fp_tag type integral_tag -let scaling_factor = 1000 +let safe_const x = + match Saturation_repr.(Option.bind (of_int_opt x) mul_safe) with + | None -> + (* because [safe_const] is always called with small enough constants. *) + assert false + | Some x -> + x + +let safe_int x = + match Saturation_repr.(of_int_opt x) with + | None -> + Saturation_repr.saturated + | Some x -> + x + +let scaling_factor = safe_const 1000 module Arith = struct type 'a t = Saturation_repr.may_saturate Saturation_repr.t @@ -38,14 +53,7 @@ module Arith = struct type integral = integral_tag t - let scaling_factor = - match - Saturation_repr.(Option.bind (of_int_opt scaling_factor) mul_safe) - with - | None -> - (* since 1000 is not saturated and mul_safe. *) assert false - | Some x -> - x + let scaling_factor = scaling_factor let sub = Saturation_repr.sub @@ -145,7 +153,9 @@ end type t = Unaccounted | Limited of {remaining : Arith.fp} -type cost = Z.t +module S = Saturation_repr + +type cost = S.may_saturate S.t let encoding = let open Data_encoding in @@ -169,44 +179,54 @@ let pp ppf = function | Limited {remaining} -> Format.fprintf ppf "%a units remaining" Arith.pp remaining -let cost_encoding = Data_encoding.z +let cost_encoding = S.z_encoding -let pp_cost fmt z = Z.pp_print fmt z +let pp_cost fmt z = S.pp fmt z -let allocation_weight = Z.of_int (scaling_factor * 2) +let allocation_weight = S.(mul_fast scaling_factor (safe_const 2)) -let step_weight = Z.of_int scaling_factor +let step_weight = scaling_factor -let read_base_weight = Z.of_int (scaling_factor * 100) +let read_base_weight = S.(mul_fast scaling_factor (safe_const 100)) -let write_base_weight = Z.of_int (scaling_factor * 160) +let write_base_weight = S.(mul_fast scaling_factor (safe_const 160)) -let byte_read_weight = Z.of_int (scaling_factor * 10) +let byte_read_weight = S.(mul_fast scaling_factor (safe_const 10)) -let byte_written_weight = Z.of_int (scaling_factor * 15) +let byte_written_weight = S.(mul_fast scaling_factor (safe_const 15)) -let cost_to_milligas (cost : cost) : Arith.fp = Arith.safe_fp cost +let cost_to_milligas (cost : cost) : Arith.fp = cost let raw_consume gas_counter cost = let gas = cost_to_milligas cost in Arith.sub_opt gas_counter gas -let alloc_cost n = Z.mul allocation_weight (Z.succ n) +let alloc_cost n = S.mul allocation_weight S.(add n (safe_const 1)) -let alloc_bytes_cost n = alloc_cost (Z.of_int ((n + 7) / 8)) +let alloc_bytes_cost n = + match S.of_int_opt ((n + 7) / 8) with + | None -> + (* Since [n] is supposed to be positive, the following case should + never occur. In case this assumption does not hold, we return + [saturated], which is always a safe cost. *) + S.saturated + | Some x -> + alloc_cost x -let atomic_step_cost n = n +let atomic_step_cost : 'a S.t -> cost = S.may_saturate -let step_cost n = Z.mul step_weight n +let step_cost n = S.mul step_weight n -let free = Z.zero +let free = S.zero |> S.may_saturate -let read_bytes_cost n = Z.add read_base_weight (Z.mul byte_read_weight n) +let read_bytes_cost n = + S.add read_base_weight (S.mul byte_read_weight (safe_int n)) -let write_bytes_cost n = Z.add write_base_weight (Z.mul byte_written_weight n) +let write_bytes_cost n = + S.add write_base_weight (S.mul byte_written_weight (safe_int n)) -let ( +@ ) x y = Z.add x y +let ( +@ ) x y = S.add x y -let ( *@ ) x y = Z.mul x y +let ( *@ ) x y = S.mul x y -let alloc_mbytes_cost n = alloc_cost (Z.of_int 12) +@ alloc_bytes_cost n +let alloc_mbytes_cost n = alloc_cost (safe_const 12) +@ alloc_bytes_cost n diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.mli b/src/proto_alpha/lib_protocol/gas_limit_repr.mli index a990ac587265..d42591fc8668 100644 --- a/src/proto_alpha/lib_protocol/gas_limit_repr.mli +++ b/src/proto_alpha/lib_protocol/gas_limit_repr.mli @@ -23,6 +23,8 @@ (* *) (*****************************************************************************) +open Saturation_repr + module Arith : Fixed_point_repr.Full type t = Unaccounted | Limited of {remaining : Arith.fp} @@ -31,7 +33,7 @@ val encoding : t Data_encoding.encoding val pp : Format.formatter -> t -> unit -type cost = Z.t +type cost = may_saturate Saturation_repr.t val cost_encoding : cost Data_encoding.encoding @@ -41,20 +43,20 @@ val raw_consume : Arith.fp -> cost -> Arith.fp option val free : cost -val atomic_step_cost : Z.t -> cost +val atomic_step_cost : _ Saturation_repr.t -> cost -val step_cost : Z.t -> cost +val step_cost : _ Saturation_repr.t -> cost -val alloc_cost : Z.t -> cost +val alloc_cost : _ Saturation_repr.t -> cost val alloc_bytes_cost : int -> cost val alloc_mbytes_cost : int -> cost -val read_bytes_cost : Z.t -> cost +val read_bytes_cost : int -> cost -val write_bytes_cost : Z.t -> cost +val write_bytes_cost : int -> cost -val ( *@ ) : Z.t -> cost -> cost +val ( *@ ) : _ Saturation_repr.t -> cost -> cost val ( +@ ) : cost -> cost -> cost diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml index d3240e7401cc..13bb0577fab7 100644 --- a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml +++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml @@ -27,23 +27,52 @@ open Alpha_context open Gas +module S = Saturation_repr module Cost_of = struct module Z_syntax = struct - (* This is a good enough approximation. Z.numbits 0 = 0 *) - let log2 x = Z.of_int (1 + Z.numbits x) - - let ( + ) = Z.add - - let ( * ) = Z.mul - - let ( lsr ) = Z.shift_right + (* This is a good enough approximation. S.numbits 0 = 0 *) + let log2 x = + match S.of_int_opt (1 + Z.numbits (S.to_z x)) with + | None -> + S.saturated + | Some x -> + x + + let ( + ) = S.add + + let ( * ) = S.mul + + let ( lsr ) (x : _ S.t) y = + match (x |> S.to_int) lsr y |> S.of_int_opt with + | None -> + S.saturated + | Some x -> + x end let z_bytes (z : Z.t) = let bits = Z.numbits z in (7 + bits) / 8 + let mul_safe_const x = + match S.(Option.bind (of_int_opt x) mul_safe) with + | None -> + (* Because [mul_safe_const] is applied to small enough literals: *) + assert false + | Some x -> + x + + let safe_const x = + match S.(of_int_opt x) with + | None -> + (* Because [safe_const] is applied to small literals: *) + assert false + | Some x -> + x + + let safe_int x = S.of_int_opt x |> S.saturate_if_undef + let int_bytes (z : 'a Script_int.num) = z_bytes (Script_int.to_zint z) let timestamp_bytes (t : Script_timestamp.t) = @@ -53,49 +82,49 @@ module Cost_of = struct (* Upper-bound on the time to compare the given value. For now, returns size in bytes, but this could get more complicated... *) let rec size_of_comparable : - type a. a Script_typed_ir.comparable_ty -> a -> Z.t = + type a. a Script_typed_ir.comparable_ty -> a -> S.may_saturate S.t = fun wit v -> match (wit, v) with | (Unit_key _, _) -> - Z.of_int 1 + safe_const 1 | (Never_key _, _) -> . | (Int_key _, _) -> - Z.of_int (int_bytes v) + safe_int @@ int_bytes v | (Nat_key _, _) -> - Z.of_int (int_bytes v) + safe_int @@ int_bytes v | (Signature_key _, _) -> - Z.of_int Signature.size + safe_const Signature.size | (String_key _, _) -> - Z.of_int (String.length v) + safe_int @@ String.length v | (Bytes_key _, _) -> - Z.of_int (Bytes.length v) + safe_int @@ Bytes.length v | (Bool_key _, _) -> - Z.of_int 8 + safe_const 8 | (Key_hash_key _, _) -> - Z.of_int Signature.Public_key_hash.size + safe_const Signature.Public_key_hash.size | (Key_key _, k) -> - Z.of_int (Signature.Public_key.size k) + safe_int @@ Signature.Public_key.size k | (Timestamp_key _, _) -> - Z.of_int (timestamp_bytes v) + safe_int @@ timestamp_bytes v | (Address_key _, _) -> - Z.of_int Signature.Public_key_hash.size + safe_const Signature.Public_key_hash.size | (Mutez_key _, _) -> - Z.of_int 8 + safe_const 8 | (Chain_id_key _, _) -> - Z.of_int Chain_id.size + safe_const Chain_id.size | (Pair_key ((l, _), (r, _), _), (lval, rval)) -> - Z.add (size_of_comparable l lval) (size_of_comparable r rval) + S.add (size_of_comparable l lval) (size_of_comparable r rval) | (Union_key ((t, _), _, _), L x) -> - Z.add (Z.of_int 1) (size_of_comparable t x) + S.add (safe_const 1) (size_of_comparable t x) | (Union_key (_, (t, _), _), R x) -> - Z.add (Z.of_int 1) (size_of_comparable t x) + S.add (safe_const 1) (size_of_comparable t x) | (Option_key _, None) -> - Z.of_int 1 + safe_const 1 | (Option_key (t, _), Some x) -> - Z.add (Z.of_int 1) (size_of_comparable t x) + S.add (safe_const 1) (size_of_comparable t x) - let manager_operation = step_cost @@ Z.of_int 1_000 + let manager_operation = step_cost @@ mul_safe_const 1_000 (* FIXME: hardcoded constant, available in next environment version. Set to a reasonable upper bound. *) @@ -106,636 +135,636 @@ module Cost_of = struct (* model N_Abs_int *) (* Approximating 0.068306 x term *) - let cost_N_Abs_int size = Z.of_int @@ (80 + (size lsr 4)) + let cost_N_Abs_int size = safe_int @@ (80 + (size lsr 4)) (* model N_Add_bls12_381_fr *) - let cost_N_Add_bls12_381_fr = Z.of_int 230 + let cost_N_Add_bls12_381_fr = safe_const 230 (* model N_Add_bls12_381_g1 *) - let cost_N_Add_bls12_381_g1 = Z.of_int 9_300 + let cost_N_Add_bls12_381_g1 = safe_const 9_300 (* model N_Add_bls12_381_g2 *) - let cost_N_Add_bls12_381_g2 = Z.of_int 13_000 + let cost_N_Add_bls12_381_g2 = safe_const 13_000 (* model N_Add_intint *) (* Approximating 0.082158 x term *) let cost_N_Add_intint size1 size2 = let v0 = Compare.Int.max size1 size2 in - Z.of_int (80 + ((v0 lsr 4) + (v0 lsr 6))) + safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) (* model N_Add_tez *) - let cost_N_Add_tez = Z.of_int 100 + let cost_N_Add_tez = safe_const 100 (* model N_And *) - let cost_N_And = Z.of_int 100 + let cost_N_And = safe_const 100 (* model N_And_nat *) (* Approximating 0.079325 x term *) let cost_N_And_nat size1 size2 = let v0 = Compare.Int.min size1 size2 in - Z.of_int (80 + ((v0 lsr 4) + (v0 lsr 6))) + safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) (* model N_Blake2b *) (* Approximating 1.366428 x term *) let cost_N_Blake2b size = let open Z_syntax in - let size = Z.of_int size in - Z.of_int 500 + (size + (size lsr 2)) + let size = safe_int size in + safe_int 500 + (size + (size lsr 2)) (* model N_Car *) - let cost_N_Car = Z.of_int 80 + let cost_N_Car = safe_const 80 (* model N_Cdr *) - let cost_N_Cdr = Z.of_int 80 + let cost_N_Cdr = safe_const 80 (* model N_Check_signature_ed25519 *) (* Approximating 1.372685 x term *) let cost_N_Check_signature_ed25519 size = let open Z_syntax in - let size = Z.of_int size in - Z.of_int 270_000 + (size + (size lsr 2)) + let size = safe_int size in + safe_const 270_000 + (size + (size lsr 2)) (* model N_Check_signature_p256 *) (* Approximating 1.385771 x term *) let cost_N_Check_signature_p256 size = let open Z_syntax in - let size = Z.of_int size in - Z.of_int 600_000 + (size + (size lsr 2) + (size lsr 3)) + let size = safe_int size in + safe_const 600_000 + (size + (size lsr 2) + (size lsr 3)) (* model N_Check_signature_secp256k1 *) (* Approximating 1.372411 x term *) let cost_N_Check_signature_secp256k1 size = let open Z_syntax in - let size = Z.of_int size in - Z.of_int 60_000 + (size + (size lsr 2)) + let size = safe_int size in + safe_const 60_000 + (size + (size lsr 2)) (* model N_Comb *) (* Approximating 3.275337 x term *) - let cost_N_Comb size = Z.of_int (80 + ((3 * size) + (size lsr 2))) + let cost_N_Comb size = safe_int (80 + ((3 * size) + (size lsr 2))) (* model N_Comb_get *) (* Approximating 0.553178 x term *) - let cost_N_Comb_get size = Z.of_int (80 + ((size lsr 1) + (size lsr 4))) + let cost_N_Comb_get size = safe_int (80 + ((size lsr 1) + (size lsr 4))) (* model N_Comb_set *) (* Approximating 1.282976 x term *) - let cost_N_Comb_set size = Z.of_int (80 + (size + (size lsr 2))) + let cost_N_Comb_set size = safe_int (80 + (size + (size lsr 2))) (* model N_Compare_address *) let cost_N_Compare_address size1 size2 = - Z.of_int (80 + (2 * Compare.Int.min size1 size2)) + safe_int (80 + (2 * Compare.Int.min size1 size2)) (* model N_Compare_bool *) let cost_N_Compare_bool size1 size2 = - Z.of_int (80 + (128 * Compare.Int.min size1 size2)) + safe_int (80 + (128 * Compare.Int.min size1 size2)) (* model N_Compare_int *) (* Approximating 0.073657 x term *) let cost_N_Compare_int size1 size2 = let v0 = Compare.Int.min size1 size2 in - Z.of_int (150 + ((v0 lsr 4) + (v0 lsr 7))) + safe_int (150 + ((v0 lsr 4) + (v0 lsr 7))) (* model N_Compare_key_hash *) let cost_N_Compare_key_hash size1 size2 = - Z.of_int (80 + (2 * Compare.Int.min size1 size2)) + safe_int (80 + (2 * Compare.Int.min size1 size2)) (* model N_Compare_mutez *) let cost_N_Compare_mutez size1 size2 = - Z.of_int (13 * Compare.Int.min size1 size2) + safe_int (13 * Compare.Int.min size1 size2) (* model N_Compare_string *) (* Approximating 0.039389 x term *) let cost_N_Compare_string size1 size2 = let v0 = Compare.Int.min size1 size2 in - Z.of_int (120 + ((v0 lsr 5) + (v0 lsr 7))) + safe_int (120 + ((v0 lsr 5) + (v0 lsr 7))) (* model N_Compare_timestamp *) (* Approximating 0.072483 x term *) let cost_N_Compare_timestamp size1 size2 = let v0 = Compare.Int.min size1 size2 in - Z.of_int (140 + ((v0 lsr 4) + (v0 lsr 7))) + safe_int (140 + ((v0 lsr 4) + (v0 lsr 7))) (* model N_Concat_string_pair *) (* Approximating 0.068808 x term *) let cost_N_Concat_string_pair size1 size2 = let open Z_syntax in - let v0 = Z.of_int size1 + Z.of_int size2 in - Z.of_int 80 + (v0 lsr 4) + let v0 = safe_int size1 + safe_int size2 in + safe_int 80 + (v0 lsr 4) (* model N_Cons_list *) - let cost_N_Cons_list = Z.of_int 80 + let cost_N_Cons_list = safe_const 80 (* model N_Cons_none *) - let cost_N_Cons_none = Z.of_int 80 + let cost_N_Cons_none = safe_const 80 (* model N_Cons_pair *) - let cost_N_Cons_pair = Z.of_int 80 + let cost_N_Cons_pair = safe_const 80 (* model N_Cons_some *) - let cost_N_Cons_some = Z.of_int 80 + let cost_N_Cons_some = safe_const 80 (* model N_Const *) - let cost_N_Const = Z.of_int 80 + let cost_N_Const = safe_const 80 (* model N_Dig *) - let cost_N_Dig size = Z.of_int (100 + (4 * size)) + let cost_N_Dig size = safe_int (100 + (4 * size)) (* model N_Dip *) - let cost_N_Dip = Z.of_int 100 + let cost_N_Dip = safe_const 100 (* model N_DipN *) - let cost_N_DipN size = Z.of_int (100 + (4 * size)) + let cost_N_DipN size = safe_int (100 + (4 * size)) (* model N_Drop *) - let cost_N_Drop = Z.of_int 80 + let cost_N_Drop = safe_const 80 (* model N_DropN *) - let cost_N_DropN size = Z.of_int (100 + (4 * size)) + let cost_N_DropN size = safe_int (100 + (4 * size)) (* model N_Dug *) - let cost_N_Dug size = Z.of_int (100 + (4 * size)) + let cost_N_Dug size = safe_int (100 + (4 * size)) (* model N_Dup *) - let cost_N_Dup = Z.of_int 80 + let cost_N_Dup = safe_int 80 (* model N_DupN *) (* Approximating 1.299969 x term *) - let cost_N_DupN size = Z.of_int (60 + size + (size lsr 2)) + let cost_N_DupN size = safe_int (60 + size + (size lsr 2)) (* model N_Ediv_natnat *) (* Approximating 0.001599 x term *) let cost_N_Ediv_natnat size1 size2 = let q = size1 - size2 in - if Compare.Int.(q < 0) then Z.of_int 300 + if Compare.Int.(q < 0) then safe_const 300 else let open Z_syntax in - let v0 = Z.of_int q * Z.of_int size2 in - Z.of_int 300 + (v0 lsr 10) + (v0 lsr 11) + (v0 lsr 13) + let v0 = safe_int q * safe_int size2 in + safe_const 300 + (v0 lsr 10) + (v0 lsr 11) + (v0 lsr 13) (* model N_Ediv_tez *) - let cost_N_Ediv_tez = Z.of_int 200 + let cost_N_Ediv_tez = safe_const 200 (* model N_Ediv_teznat *) (* Extracted by hand from the empirical data *) - let cost_N_Ediv_teznat = Z.of_int 300 + let cost_N_Ediv_teznat = safe_const 300 (* model N_Empty_map *) - let cost_N_Empty_map = Z.of_int 240 + let cost_N_Empty_map = safe_const 240 (* model N_Empty_set *) - let cost_N_Empty_set = Z.of_int 240 + let cost_N_Empty_set = safe_const 240 (* model N_Eq *) - let cost_N_Eq = Z.of_int 80 + let cost_N_Eq = safe_const 80 (* model N_If *) - let cost_N_If = Z.of_int 60 + let cost_N_If = safe_const 60 (* model N_If_cons *) - let cost_N_If_cons = Z.of_int 110 + let cost_N_If_cons = safe_const 110 (* model N_If_left *) - let cost_N_If_left = Z.of_int 90 + let cost_N_If_left = safe_const 90 (* model N_If_none *) - let cost_N_If_none = Z.of_int 80 + let cost_N_If_none = safe_const 80 (* model N_Int_nat *) - let cost_N_Int_nat = Z.of_int 80 + let cost_N_Int_nat = safe_const 80 (* model N_Is_nat *) - let cost_N_Is_nat = Z.of_int 80 + let cost_N_Is_nat = safe_const 80 (* model N_Keccak *) let cost_N_Keccak size = let open Z_syntax in - Z.of_int 1_400 + (Z.of_int 30 * Z.of_int size) + safe_const 1_400 + (safe_const 30 * safe_int size) (* model N_Left *) - let cost_N_Left = Z.of_int 80 + let cost_N_Left = safe_const 80 (* model N_List_iter *) let cost_N_List_iter size = let open Z_syntax in - Z.of_int 500 + (Z.of_int 7 * Z.of_int size) + safe_const 500 + (safe_const 7 * safe_int size) (* model N_List_map *) let cost_N_List_map size = let open Z_syntax in - Z.of_int 500 + (Z.of_int 12 * Z.of_int size) + safe_const 500 + (safe_const 12 * safe_int size) (* model N_List_size *) - let cost_N_List_size = Z.of_int 80 + let cost_N_List_size = safe_const 80 (* model N_Loop *) - let cost_N_Loop = Z.of_int 70 + let cost_N_Loop = safe_const 70 (* model N_Loop_left *) - let cost_N_Loop_left = Z.of_int 80 + let cost_N_Loop_left = safe_const 80 (* model N_Lsl_nat *) (* Approximating 0.129443 x term *) - let cost_N_Lsl_nat size = Z.of_int (150 + (size lsr 3)) + let cost_N_Lsl_nat size = safe_int (150 + (size lsr 3)) (* model N_Lsr_nat *) (* Approximating 0.129435 x term *) - let cost_N_Lsr_nat size = Z.of_int (150 + (size lsr 3)) + let cost_N_Lsr_nat size = safe_int (150 + (size lsr 3)) (* model N_Map_get *) (* Approximating 0.057548 x term *) let cost_N_Map_get size1 size2 = let open Z_syntax in - let v0 = size1 * log2 (Z.of_int size2) in - Z.of_int 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) + let v0 = size1 * log2 size2 in + safe_const 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) (* model N_Map_iter *) let cost_N_Map_iter size = let open Z_syntax in - Z.of_int 80 + (Z.of_int 40 * Z.of_int size) + safe_const 80 + (safe_const 40 * safe_int size) (* model N_Map_map *) let cost_N_Map_map size = let open Z_syntax in - Z.of_int 80 + (Z.of_int 761 * Z.of_int size) + safe_const 80 + (safe_const 761 * safe_int size) (* model N_Map_mem *) (* Approximating 0.058563 x term *) let cost_N_Map_mem size1 size2 = let open Z_syntax in - let v0 = size1 * log2 (Z.of_int size2) in - Z.of_int 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) + let v0 = size1 * log2 size2 in + safe_const 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) (* model N_Map_size *) - let cost_N_Map_size = Z.of_int 90 + let cost_N_Map_size = safe_const 90 (* model N_Map_update *) (* Approximating 0.119968 x term *) let cost_N_Map_update size1 size2 = let open Z_syntax in - let v0 = size1 * log2 (Z.of_int size2) in - Z.of_int 80 + (v0 lsr 4) + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) + let v0 = size1 * log2 size2 in + safe_const 80 + (v0 lsr 4) + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) (* model N_Mul_bls12_381_fr *) - let cost_N_Mul_bls12_381_fr = Z.of_int 260 + let cost_N_Mul_bls12_381_fr = safe_const 260 (* model N_Mul_bls12_381_g1 *) - let cost_N_Mul_bls12_381_g1 = Z.of_int 265_000 + let cost_N_Mul_bls12_381_g1 = safe_const 265_000 (* model N_Mul_bls12_381_g2 *) - let cost_N_Mul_bls12_381_g2 = Z.of_int 850_000 + let cost_N_Mul_bls12_381_g2 = safe_const 850_000 - (* Converting fr from/to Z.t *) - let cost_bls12_381_fr_of_z = Z.of_int 130 + (* Converting fr from/to S.t *) + let cost_bls12_381_fr_of_z = safe_const 130 - let cost_bls12_381_fr_to_z = Z.of_int 30 + let cost_bls12_381_fr_to_z = safe_const 30 let cost_N_Mul_bls12_381_fr_z = - Z.add cost_bls12_381_fr_of_z cost_N_Mul_bls12_381_fr + S.add cost_bls12_381_fr_of_z cost_N_Mul_bls12_381_fr let cost_N_Int_bls12_381_fr = cost_bls12_381_fr_to_z (* model N_Mul_intint *) let cost_N_Mul_intint size1 size2 = let open Z_syntax in - let a = Z.of_int size1 + Z.of_int size2 in - Z.of_int 80 + (a * log2 a) + let a = S.add (safe_int size1) (safe_int size2) in + safe_const 80 + (a * log2 a) (* model N_Mul_teznat *) let cost_N_Mul_teznat size = let open Z_syntax in - Z.of_int 200 + (Z.of_int 133 * Z.of_int size) + safe_const 200 + (safe_const 133 * safe_int size) (* model N_Neg_bls12_381_fr *) - let cost_N_Neg_bls12_381_fr = Z.of_int 180 + let cost_N_Neg_bls12_381_fr = safe_const 180 (* model N_Neg_bls12_381_g1 *) - let cost_N_Neg_bls12_381_g1 = Z.of_int 410 + let cost_N_Neg_bls12_381_g1 = safe_const 410 (* model N_Neg_bls12_381_g2 *) - let cost_N_Neg_bls12_381_g2 = Z.of_int 715 + let cost_N_Neg_bls12_381_g2 = safe_const 715 (* model N_Neg_int *) (* Approximating 0.068419 x term *) - let cost_N_Neg_int size = Z.of_int (80 + (size lsr 4)) + let cost_N_Neg_int size = safe_int (80 + (size lsr 4)) (* model N_Neq *) - let cost_N_Neq = Z.of_int 80 + let cost_N_Neq = safe_const 80 (* model N_Nil *) - let cost_N_Nil = Z.of_int 80 + let cost_N_Nil = safe_const 80 (* model N_Nop *) - let cost_N_Nop = Z.of_int 70 + let cost_N_Nop = safe_const 70 (* model N_Not *) - let cost_N_Not = Z.of_int 90 + let cost_N_Not = safe_const 90 (* model N_Not_int *) (* Approximating 0.076564 x term *) - let cost_N_Not_int size = Z.of_int (55 + ((size lsr 4) + (size lsr 7))) + let cost_N_Not_int size = safe_int (55 + ((size lsr 4) + (size lsr 7))) (* model N_Or *) - let cost_N_Or = Z.of_int 90 + let cost_N_Or = safe_const 90 (* model N_Or_nat *) (* Approximating 0.078718 x term *) let cost_N_Or_nat size1 size2 = let v0 = Compare.Int.max size1 size2 in - Z.of_int (80 + ((v0 lsr 4) + (v0 lsr 6))) + safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) (* model N_Pairing_check_bls12_381 *) let cost_N_Pairing_check_bls12_381 size = - Z.add (Z.of_int 1_550_000) (Z.mul (Z.of_int 510_000) (Z.of_int size)) + S.add (safe_const 1_550_000) (S.mul (safe_const 510_000) (safe_int size)) (* model N_Right *) - let cost_N_Right = Z.of_int 80 + let cost_N_Right = safe_const 80 (* model N_Seq *) - let cost_N_Seq = Z.of_int 60 + let cost_N_Seq = safe_const 60 (* model N_Set_iter *) let cost_N_Set_iter size = let open Z_syntax in - Z.of_int 80 + (Z.of_int 36 * Z.of_int size) + safe_const 80 + (safe_const 36 * safe_int size) (* model N_Set_mem *) (* Approximating 0.059410 x term *) let cost_N_Set_mem size1 size2 = let open Z_syntax in - let v0 = size1 * log2 (Z.of_int size2) in - Z.of_int 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) + (v0 lsr 8) + let v0 = size1 * log2 (safe_int size2) in + safe_const 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) + (v0 lsr 8) (* model N_Set_size *) - let cost_N_Set_size = Z.of_int 80 + let cost_N_Set_size = safe_const 80 (* model N_Set_update *) (* Approximating 0.126260 x term *) let cost_N_Set_update size1 size2 = let open Z_syntax in - let v0 = size1 * log2 (Z.of_int size2) in - Z.of_int 80 + (v0 lsr 3) + let v0 = size1 * log2 (safe_int size2) in + safe_const 80 + (v0 lsr 3) (* model N_Sha256 *) let cost_N_Sha256 size = let open Z_syntax in - Z.of_int 500 + (Z.of_int 5 * Z.of_int size) + safe_const 500 + (safe_const 5 * safe_int size) (* model N_Sha3 *) let cost_N_Sha3 size = let open Z_syntax in - Z.of_int 1_400 + (Z.of_int 32 * Z.of_int size) + safe_const 1_400 + (safe_const 32 * safe_int size) (* model N_Sha512 *) let cost_N_Sha512 size = let open Z_syntax in - Z.of_int 500 + (Z.of_int 3 * Z.of_int size) + safe_const 500 + (safe_const 3 * safe_int size) (* model N_Slice_string *) (* Approximating 0.067048 x term *) - let cost_N_Slice_string size = Z.of_int (80 + (size lsr 4)) + let cost_N_Slice_string size = safe_int (80 + (size lsr 4)) (* model N_String_size *) - let cost_N_String_size = Z.of_int 80 + let cost_N_String_size = safe_const 80 (* model N_Sub_int *) (* Approximating 0.082399 x term *) let cost_N_Sub_int size1 size2 = let v0 = Compare.Int.max size1 size2 in - Z.of_int (80 + ((v0 lsr 4) + (v0 lsr 6))) + safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) (* model N_Sub_tez *) - let cost_N_Sub_tez = Z.of_int 80 + let cost_N_Sub_tez = safe_const 80 (* model N_Swap *) - let cost_N_Swap = Z.of_int 70 + let cost_N_Swap = safe_const 70 (* model N_Total_voting_power *) - let cost_N_Total_voting_power = Z.of_int 400 + let cost_N_Total_voting_power = safe_const 400 (* model N_Uncomb *) (* Approximating 3.666332 x term *) let cost_N_Uncomb size = - Z.of_int (80 + ((3 * size) + (size lsr 1) + (size lsr 3))) + safe_int (80 + ((3 * size) + (size lsr 1) + (size lsr 3))) (* model N_Unpair *) - let cost_N_Unpair = Z.of_int 80 + let cost_N_Unpair = safe_const 80 (* model N_Voting_power *) - let cost_N_Voting_power = Z.of_int 400 + let cost_N_Voting_power = safe_const 400 (* model N_Xor *) - let cost_N_Xor = Z.of_int 100 + let cost_N_Xor = safe_const 100 (* model N_Xor_nat *) (* Approximating 0.078258 x term *) let cost_N_Xor_nat size1 size2 = let v0 = Compare.Int.max size1 size2 in - Z.of_int (80 + ((v0 lsr 4) + (v0 lsr 6))) + safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) (* model DECODING_BLS_FR *) - let cost_DECODING_BLS_FR = Z.of_int 50 + let cost_DECODING_BLS_FR = mul_safe_const 50 (* model DECODING_BLS_G1 *) - let cost_DECODING_BLS_G1 = Z.of_int 230_000 + let cost_DECODING_BLS_G1 = mul_safe_const 230_000 (* model DECODING_BLS_G2 *) - let cost_DECODING_BLS_G2 = Z.of_int 740_000 + let cost_DECODING_BLS_G2 = safe_const 740_000 (* model B58CHECK_DECODING_CHAIN_ID *) - let cost_B58CHECK_DECODING_CHAIN_ID = Z.of_int 1_500 + let cost_B58CHECK_DECODING_CHAIN_ID = safe_const 1_500 (* model B58CHECK_DECODING_PUBLIC_KEY_HASH_ed25519 *) - let cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_ed25519 = Z.of_int 3_300 + let cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_ed25519 = safe_const 3_300 (* model B58CHECK_DECODING_PUBLIC_KEY_HASH_p256 *) - let cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_p256 = Z.of_int 3_300 + let cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_p256 = safe_const 3_300 (* model B58CHECK_DECODING_PUBLIC_KEY_HASH_secp256k1 *) - let cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_secp256k1 = Z.of_int 3_300 + let cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_secp256k1 = safe_const 3_300 (* model B58CHECK_DECODING_PUBLIC_KEY_ed25519 *) - let cost_B58CHECK_DECODING_PUBLIC_KEY_ed25519 = Z.of_int 4_300 + let cost_B58CHECK_DECODING_PUBLIC_KEY_ed25519 = safe_const 4_300 (* model B58CHECK_DECODING_PUBLIC_KEY_p256 *) - let cost_B58CHECK_DECODING_PUBLIC_KEY_p256 = Z.of_int 29_000 + let cost_B58CHECK_DECODING_PUBLIC_KEY_p256 = safe_const 29_000 (* model B58CHECK_DECODING_PUBLIC_KEY_secp256k1 *) - let cost_B58CHECK_DECODING_PUBLIC_KEY_secp256k1 = Z.of_int 9_400 + let cost_B58CHECK_DECODING_PUBLIC_KEY_secp256k1 = safe_const 9_400 (* model B58CHECK_DECODING_SIGNATURE_ed25519 *) - let cost_B58CHECK_DECODING_SIGNATURE_ed25519 = Z.of_int 6_600 + let cost_B58CHECK_DECODING_SIGNATURE_ed25519 = safe_const 6_600 (* model B58CHECK_DECODING_SIGNATURE_p256 *) - let cost_B58CHECK_DECODING_SIGNATURE_p256 = Z.of_int 6_600 + let cost_B58CHECK_DECODING_SIGNATURE_p256 = safe_const 6_600 (* model B58CHECK_DECODING_SIGNATURE_secp256k1 *) - let cost_B58CHECK_DECODING_SIGNATURE_secp256k1 = Z.of_int 6_600 + let cost_B58CHECK_DECODING_SIGNATURE_secp256k1 = safe_const 6_600 (* model ENCODING_BLS_FR *) - let cost_ENCODING_BLS_FR = Z.of_int 30 + let cost_ENCODING_BLS_FR = safe_const 30 (* model ENCODING_BLS_G1 *) - let cost_ENCODING_BLS_G1 = Z.of_int 30 + let cost_ENCODING_BLS_G1 = safe_const 30 (* model ENCODING_BLS_G2 *) - let cost_ENCODING_BLS_G2 = Z.of_int 30 + let cost_ENCODING_BLS_G2 = safe_const 30 (* model B58CHECK_ENCODING_CHAIN_ID *) - let cost_B58CHECK_ENCODING_CHAIN_ID = Z.of_int 1_600 + let cost_B58CHECK_ENCODING_CHAIN_ID = safe_const 1_600 (* model B58CHECK_ENCODING_PUBLIC_KEY_HASH_ed25519 *) - let cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_ed25519 = Z.of_int 3_300 + let cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_ed25519 = safe_const 3_300 (* model B58CHECK_ENCODING_PUBLIC_KEY_HASH_p256 *) - let cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_p256 = Z.of_int 3_750 + let cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_p256 = safe_const 3_750 (* model B58CHECK_ENCODING_PUBLIC_KEY_HASH_secp256k1 *) - let cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_secp256k1 = Z.of_int 3_300 + let cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_secp256k1 = safe_const 3_300 (* model B58CHECK_ENCODING_PUBLIC_KEY_ed25519 *) - let cost_B58CHECK_ENCODING_PUBLIC_KEY_ed25519 = Z.of_int 4_500 + let cost_B58CHECK_ENCODING_PUBLIC_KEY_ed25519 = safe_const 4_500 (* model B58CHECK_ENCODING_PUBLIC_KEY_p256 *) - let cost_B58CHECK_ENCODING_PUBLIC_KEY_p256 = Z.of_int 5_300 + let cost_B58CHECK_ENCODING_PUBLIC_KEY_p256 = safe_const 5_300 (* model B58CHECK_ENCODING_PUBLIC_KEY_secp256k1 *) - let cost_B58CHECK_ENCODING_PUBLIC_KEY_secp256k1 = Z.of_int 5_000 + let cost_B58CHECK_ENCODING_PUBLIC_KEY_secp256k1 = safe_const 5_000 (* model B58CHECK_ENCODING_SIGNATURE_ed25519 *) - let cost_B58CHECK_ENCODING_SIGNATURE_ed25519 = Z.of_int 8_700 + let cost_B58CHECK_ENCODING_SIGNATURE_ed25519 = safe_const 8_700 (* model B58CHECK_ENCODING_SIGNATURE_p256 *) - let cost_B58CHECK_ENCODING_SIGNATURE_p256 = Z.of_int 8_700 + let cost_B58CHECK_ENCODING_SIGNATURE_p256 = safe_const 8_700 (* model B58CHECK_ENCODING_SIGNATURE_secp256k1 *) - let cost_B58CHECK_ENCODING_SIGNATURE_secp256k1 = Z.of_int 8_700 + let cost_B58CHECK_ENCODING_SIGNATURE_secp256k1 = safe_const 8_700 (* model DECODING_CHAIN_ID *) - let cost_DECODING_CHAIN_ID = Z.of_int 50 + let cost_DECODING_CHAIN_ID = safe_const 50 (* model DECODING_PUBLIC_KEY_HASH_ed25519 *) - let cost_DECODING_PUBLIC_KEY_HASH_ed25519 = Z.of_int 50 + let cost_DECODING_PUBLIC_KEY_HASH_ed25519 = safe_const 50 (* model DECODING_PUBLIC_KEY_HASH_p256 *) - let cost_DECODING_PUBLIC_KEY_HASH_p256 = Z.of_int 60 + let cost_DECODING_PUBLIC_KEY_HASH_p256 = safe_const 60 (* model DECODING_PUBLIC_KEY_HASH_secp256k1 *) - let cost_DECODING_PUBLIC_KEY_HASH_secp256k1 = Z.of_int 60 + let cost_DECODING_PUBLIC_KEY_HASH_secp256k1 = safe_const 60 (* model DECODING_PUBLIC_KEY_ed25519 *) - let cost_DECODING_PUBLIC_KEY_ed25519 = Z.of_int 60 + let cost_DECODING_PUBLIC_KEY_ed25519 = safe_const 60 (* model DECODING_PUBLIC_KEY_p256 *) - let cost_DECODING_PUBLIC_KEY_p256 = Z.of_int 25_000 + let cost_DECODING_PUBLIC_KEY_p256 = safe_const 25_000 (* model DECODING_PUBLIC_KEY_secp256k1 *) - let cost_DECODING_PUBLIC_KEY_secp256k1 = Z.of_int 5_300 + let cost_DECODING_PUBLIC_KEY_secp256k1 = safe_const 5_300 (* model DECODING_SIGNATURE_ed25519 *) - let cost_DECODING_SIGNATURE_ed25519 = Z.of_int 30 + let cost_DECODING_SIGNATURE_ed25519 = safe_const 30 (* model DECODING_SIGNATURE_p256 *) - let cost_DECODING_SIGNATURE_p256 = Z.of_int 30 + let cost_DECODING_SIGNATURE_p256 = safe_const 30 (* model DECODING_SIGNATURE_secp256k1 *) - let cost_DECODING_SIGNATURE_secp256k1 = Z.of_int 30 + let cost_DECODING_SIGNATURE_secp256k1 = safe_const 30 (* model ENCODING_CHAIN_ID *) - let cost_ENCODING_CHAIN_ID = Z.of_int 50 + let cost_ENCODING_CHAIN_ID = safe_const 50 (* model ENCODING_PUBLIC_KEY_HASH_ed25519 *) - let cost_ENCODING_PUBLIC_KEY_HASH_ed25519 = Z.of_int 70 + let cost_ENCODING_PUBLIC_KEY_HASH_ed25519 = safe_const 70 (* model ENCODING_PUBLIC_KEY_HASH_p256 *) - let cost_ENCODING_PUBLIC_KEY_HASH_p256 = Z.of_int 80 + let cost_ENCODING_PUBLIC_KEY_HASH_p256 = safe_const 80 (* model ENCODING_PUBLIC_KEY_HASH_secp256k1 *) - let cost_ENCODING_PUBLIC_KEY_HASH_secp256k1 = Z.of_int 70 + let cost_ENCODING_PUBLIC_KEY_HASH_secp256k1 = safe_const 70 (* model ENCODING_PUBLIC_KEY_ed25519 *) - let cost_ENCODING_PUBLIC_KEY_ed25519 = Z.of_int 80 + let cost_ENCODING_PUBLIC_KEY_ed25519 = safe_const 80 (* model ENCODING_PUBLIC_KEY_p256 *) - let cost_ENCODING_PUBLIC_KEY_p256 = Z.of_int 450 + let cost_ENCODING_PUBLIC_KEY_p256 = safe_const 450 (* model ENCODING_PUBLIC_KEY_secp256k1 *) - let cost_ENCODING_PUBLIC_KEY_secp256k1 = Z.of_int 490 + let cost_ENCODING_PUBLIC_KEY_secp256k1 = safe_const 490 (* model ENCODING_SIGNATURE_ed25519 *) - let cost_ENCODING_SIGNATURE_ed25519 = Z.of_int 40 + let cost_ENCODING_SIGNATURE_ed25519 = safe_const 40 (* model ENCODING_SIGNATURE_p256 *) - let cost_ENCODING_SIGNATURE_p256 = Z.of_int 40 + let cost_ENCODING_SIGNATURE_p256 = safe_const 40 (* model ENCODING_SIGNATURE_secp256k1 *) - let cost_ENCODING_SIGNATURE_secp256k1 = Z.of_int 40 + let cost_ENCODING_SIGNATURE_secp256k1 = safe_const 40 (* model TIMESTAMP_READABLE_DECODING *) - let cost_TIMESTAMP_READABLE_DECODING = Z.of_int 130 + let cost_TIMESTAMP_READABLE_DECODING = safe_const 130 (* model TIMESTAMP_READABLE_ENCODING *) - let cost_TIMESTAMP_READABLE_ENCODING = Z.of_int 900 + let cost_TIMESTAMP_READABLE_ENCODING = safe_const 900 (* model CHECK_PRINTABLE *) let cost_CHECK_PRINTABLE size = let open Z_syntax in - Z.of_int 14 + (Z.of_int 10 * Z.of_int size) + safe_const 14 + (safe_const 10 * safe_int size) (* model MERGE_TYPES This is the estimated cost of one iteration of merge_types, extracted and copied manually from the parameter fit for the MERGE_TYPES benchmark (the model is parametric on the size of the type, which we don't have access to in O(1)). *) - let cost_MERGE_TYPES = Z.of_int 130 + let cost_MERGE_TYPES = safe_const 130 (* model TYPECHECKING_CODE This is the cost of one iteration of parse_instr, extracted by hand from the parameter fit for the TYPECHECKING_CODE benchmark. *) - let cost_TYPECHECKING_CODE = Z.of_int 375 + let cost_TYPECHECKING_CODE = safe_const 375 (* model UNPARSING_CODE This is the cost of one iteration of unparse_instr, extracted by hand from the parameter fit for the UNPARSING_CODE benchmark. *) - let cost_UNPARSING_CODE = Z.of_int 200 + let cost_UNPARSING_CODE = safe_const 200 (* model TYPECHECKING_DATA This is the cost of one iteration of parse_data, extracted by hand from the parameter fit for the TYPECHECKING_DATA benchmark. *) - let cost_TYPECHECKING_DATA = Z.of_int 240 + let cost_TYPECHECKING_DATA = safe_const 240 (* model UNPARSING_DATA This is the cost of one iteration of unparse_data, extracted by hand from the parameter fit for the UNPARSING_DATA benchmark. *) - let cost_UNPARSING_DATA = Z.of_int 140 + let cost_UNPARSING_DATA = safe_const 140 (* model PARSE_TYPE This is the cost of one iteration of parse_ty, extracted by hand from the parameter fit for the PARSE_TYPE benchmark. *) - let cost_PARSE_TYPE = Z.of_int 170 + let cost_PARSE_TYPE = safe_const 170 (* model UNPARSE_TYPE This is the cost of one iteration of unparse_ty, extracted by hand from the parameter fit for the UNPARSE_TYPE benchmark. *) - let cost_UNPARSE_TYPE = Z.of_int 185 + let cost_UNPARSE_TYPE = safe_const 185 (* TODO: benchmark *) - let cost_COMPARABLE_TY_OF_TY = Z.of_int 120 + let cost_COMPARABLE_TY_OF_TY = safe_const 120 end module Interpreter = struct @@ -809,17 +838,17 @@ module Cost_of = struct let map_mem (type k v) (elt : k) ((module Box) : (k, v) Script_typed_ir.map) = let elt_size = size_of_comparable Box.key_ty elt in - atomic_step_cost (cost_N_Map_mem elt_size (snd Box.boxed)) + atomic_step_cost (cost_N_Map_mem elt_size (safe_int (snd Box.boxed))) let map_get (type k v) (elt : k) ((module Box) : (k, v) Script_typed_ir.map) = let elt_size = size_of_comparable Box.key_ty elt in - atomic_step_cost (cost_N_Map_get elt_size (snd Box.boxed)) + atomic_step_cost (cost_N_Map_get elt_size (safe_int (snd Box.boxed))) let map_update (type k v) (elt : k) ((module Box) : (k, v) Script_typed_ir.map) = let elt_size = size_of_comparable Box.key_ty elt in - atomic_step_cost (cost_N_Map_update elt_size (snd Box.boxed)) + atomic_step_cost (cost_N_Map_update elt_size (safe_int (snd Box.boxed))) let map_get_and_update (type k v) (elt : k) (m : (k, v) Script_typed_ir.map) = @@ -1008,21 +1037,21 @@ module Cost_of = struct let sapling_verify_update ~inputs ~outputs = let open Z_syntax in atomic_step_cost - ( Z.of_int 85_000 - + (Z.of_int inputs * Z.of_int 4) - + (Z.of_int outputs * Z.of_int 30) ) + ( safe_const 85_000 + + (safe_int inputs * safe_int 4) + + (safe_int outputs * safe_int 30) ) (* --------------------------------------------------------------------- *) (* Semi-hand-crafted models *) - let compare_unit = atomic_step_cost (Z.of_int 10) + let compare_unit = atomic_step_cost (safe_int 10) - let compare_union_tag = atomic_step_cost (Z.of_int 10) + let compare_union_tag = atomic_step_cost (safe_const 10) - let compare_option_tag = atomic_step_cost (Z.of_int 10) + let compare_option_tag = atomic_step_cost (safe_const 10) let compare_bool = atomic_step_cost (cost_N_Compare_bool 1 1) - let compare_signature = atomic_step_cost (Z.of_int 92) + let compare_signature = atomic_step_cost (safe_const 92) let compare_string s1 s2 = atomic_step_cost @@ -1044,7 +1073,7 @@ module Cost_of = struct let sz = Signature.Public_key_hash.size in atomic_step_cost (cost_N_Compare_key_hash sz sz) - let compare_key = atomic_step_cost (Z.of_int 92) + let compare_key = atomic_step_cost (safe_const 92) let compare_timestamp t1 t2 = atomic_step_cost @@ -1056,7 +1085,7 @@ module Cost_of = struct let sz = Signature.Public_key_hash.size + Chain_id.size in atomic_step_cost (cost_N_Compare_address sz sz) - let compare_chain_id = atomic_step_cost (Z.of_int 30) + let compare_chain_id = atomic_step_cost (safe_const 30) let rec compare : type a. a Script_typed_ir.comparable_ty -> a -> a -> cost = @@ -1136,25 +1165,25 @@ module Cost_of = struct *) let concat_string_precheck (l : 'a Script_typed_ir.boxed_list) = (* we set the precheck to be slightly more expensive than cost_N_List_iter *) - atomic_step_cost (Z.mul (Z.of_int l.length) (Z.of_int 10)) + atomic_step_cost (S.mul (safe_int l.length) (safe_const 10)) (* This is the cost of allocating a string and blitting existing ones into it. *) let concat_string total_bytes = atomic_step_cost - Z.(add (of_int 100) (fst (ediv_rem total_bytes (of_int 10)))) + S.(add (safe_int 100) (S.ediv total_bytes (safe_int 10))) (* Same story as Concat_string. *) let concat_bytes total_bytes = atomic_step_cost - Z.(add (of_int 100) (fst (ediv_rem total_bytes (of_int 10)))) + S.(add (safe_int 100) (S.ediv total_bytes (safe_int 10))) (* Cost of additional call to logger + overhead of setting up call to [interp]. *) - let exec = atomic_step_cost (Z.of_int 100) + let exec = atomic_step_cost (safe_const 100) (* Heavy computation happens in the [unparse_data], [unparse_ty] functions which are carbonated. We must account for allocating the Micheline lambda wrapper. *) - let apply = atomic_step_cost (Z.of_int 1000) + let apply = atomic_step_cost (safe_const 1000) (* Pushing a pointer on the stack. *) let lambda = push @@ -1186,7 +1215,7 @@ module Cost_of = struct let balance = Gas.free (* Accessing the raw_context, Small arithmetic & pushing on the stack. *) - let level = atomic_step_cost (Z.mul (Z.of_int 2) cost_N_Const) + let level = atomic_step_cost (S.mul (safe_const 2) cost_N_Const) (* Same as [cost_level] *) let now = level @@ -1217,15 +1246,17 @@ module Cost_of = struct let unpack_failed bytes = (* We cannot instrument failed deserialization, so we take worst case fees: a set of size 1 bytes values. *) - let len = Z.of_int (Bytes.length bytes) in + let blen = Bytes.length bytes in + let len = safe_int blen in + let d = Z.numbits (Z.of_int blen) in (len *@ alloc_mbytes_cost 1) +@ len - *@ ( Z.of_int (Z.numbits len) - *@ (alloc_cost (Z.of_int 3) +@ step_cost Z.one) ) + *@ ( safe_int d + *@ (alloc_cost (safe_const 3) +@ step_cost (safe_const 1)) ) - let ticket = atomic_step_cost (Z.of_int 80) + let ticket = atomic_step_cost (safe_const 80) - let read_ticket = atomic_step_cost (Z.of_int 80) + let read_ticket = atomic_step_cost (safe_const 80) let split_ticket ticket_amount amount_a amount_b = ticket @@ -1248,7 +1279,7 @@ module Cost_of = struct let public_key_optimized = atomic_step_cost - @@ Compare.Z.( + @@ S.( max cost_DECODING_PUBLIC_KEY_ed25519 (max @@ -1257,7 +1288,7 @@ module Cost_of = struct let public_key_readable = atomic_step_cost - @@ Compare.Z.( + @@ S.( max cost_B58CHECK_DECODING_PUBLIC_KEY_ed25519 (max @@ -1266,7 +1297,7 @@ module Cost_of = struct let key_hash_optimized = atomic_step_cost - @@ Compare.Z.( + @@ S.( max cost_DECODING_PUBLIC_KEY_HASH_ed25519 (max @@ -1275,7 +1306,7 @@ module Cost_of = struct let key_hash_readable = atomic_step_cost - @@ Compare.Z.( + @@ S.( max cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_ed25519 (max @@ -1284,7 +1315,7 @@ module Cost_of = struct let signature_optimized = atomic_step_cost - @@ Compare.Z.( + @@ S.( max cost_DECODING_SIGNATURE_ed25519 (max @@ -1293,7 +1324,7 @@ module Cost_of = struct let signature_readable = atomic_step_cost - @@ Compare.Z.( + @@ S.( max cost_B58CHECK_DECODING_SIGNATURE_ed25519 (max @@ -1343,7 +1374,7 @@ module Cost_of = struct let timestamp_readable = atomic_step_cost cost_TIMESTAMP_READABLE_DECODING (* Reasonable estimate. *) - let contract = Gas.(Z.of_int 2 *@ public_key_readable) + let contract = Gas.(safe_const 2 *@ public_key_readable) (* Assuming unflattened storage: /contracts/hash1/.../hash6/key/balance, balance stored on 64 bits *) @@ -1353,7 +1384,8 @@ module Cost_of = struct (* Constructing proof arguments consists in a decreasing loop in the result monad, allocating at each step. We charge a reasonable overapproximation. *) - let proof_argument n = atomic_step_cost (Z.mul (Z.of_int n) (Z.of_int 50)) + let proof_argument n = + atomic_step_cost (S.mul (safe_int n) (safe_const 50)) end module Unparsing = struct @@ -1361,7 +1393,7 @@ module Cost_of = struct let public_key_optimized = atomic_step_cost - @@ Compare.Z.( + @@ S.( max cost_ENCODING_PUBLIC_KEY_ed25519 (max @@ -1370,7 +1402,7 @@ module Cost_of = struct let public_key_readable = atomic_step_cost - @@ Compare.Z.( + @@ S.( max cost_B58CHECK_ENCODING_PUBLIC_KEY_ed25519 (max @@ -1379,7 +1411,7 @@ module Cost_of = struct let key_hash_optimized = atomic_step_cost - @@ Compare.Z.( + @@ S.( max cost_ENCODING_PUBLIC_KEY_HASH_ed25519 (max @@ -1388,7 +1420,7 @@ module Cost_of = struct let key_hash_readable = atomic_step_cost - @@ Compare.Z.( + @@ S.( max cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_ed25519 (max @@ -1397,7 +1429,7 @@ module Cost_of = struct let signature_optimized = atomic_step_cost - @@ Compare.Z.( + @@ S.( max cost_ENCODING_SIGNATURE_ed25519 (max @@ -1406,7 +1438,7 @@ module Cost_of = struct let signature_readable = atomic_step_cost - @@ Compare.Z.( + @@ S.( max cost_B58CHECK_ENCODING_SIGNATURE_ed25519 (max @@ -1443,7 +1475,7 @@ module Cost_of = struct let unit = Gas.free (* Reasonable estimate. *) - let contract = Gas.(Z.of_int 2 *@ public_key_readable) + let contract = Gas.(safe_const 2 *@ public_key_readable) (* Reuse 006 costs. *) let operation bytes = Script.bytes_node_cost bytes diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.mli b/src/proto_alpha/lib_protocol/michelson_v1_gas.mli index 1ed46de6eed6..5944a5ba983a 100644 --- a/src/proto_alpha/lib_protocol/michelson_v1_gas.mli +++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.mli @@ -243,9 +243,11 @@ module Cost_of : sig val concat_string_precheck : 'a Script_typed_ir.boxed_list -> Gas.cost - val concat_string : Z.t -> Gas.cost + val concat_string : + Saturation_repr.may_saturate Saturation_repr.t -> Gas.cost - val concat_bytes : Z.t -> Gas.cost + val concat_bytes : + Saturation_repr.may_saturate Saturation_repr.t -> Gas.cost val exec : Gas.cost diff --git a/src/proto_alpha/lib_protocol/sapling_storage.ml b/src/proto_alpha/lib_protocol/sapling_storage.ml index 82dfef527794..7e7c63106a7c 100644 --- a/src/proto_alpha/lib_protocol/sapling_storage.ml +++ b/src/proto_alpha/lib_protocol/sapling_storage.ml @@ -411,9 +411,11 @@ let apply_diff ctx id diff = let open Sapling_repr in let nb_commitments = List.length diff.commitments_and_ciphertexts in let nb_nullifiers = List.length diff.nullifiers in - Raw_context.consume_gas - ctx - (sapling_apply_diff_cost ~inputs:nb_nullifiers ~outputs:nb_commitments) + let sapling_cost = + sapling_apply_diff_cost ~inputs:nb_nullifiers ~outputs:nb_commitments + |> Saturation_repr.of_z_opt |> Saturation_repr.saturate_if_undef + in + Raw_context.consume_gas ctx sapling_cost >>?= fun ctx -> Storage.Sapling.Commitments_size.get (ctx, id) >>=? fun cm_start_pos -> diff --git a/src/proto_alpha/lib_protocol/saturation_repr.ml b/src/proto_alpha/lib_protocol/saturation_repr.ml index 824fabbeb589..1ecfaf90c160 100644 --- a/src/proto_alpha/lib_protocol/saturation_repr.ml +++ b/src/proto_alpha/lib_protocol/saturation_repr.ml @@ -64,6 +64,10 @@ let of_z_opt z = let to_z x = Z.of_int x +let saturate_if_undef = function None -> saturated | Some x -> x + +let safe_int x = of_int_opt x |> saturate_if_undef + let zero = 0 let small_enough z = diff --git a/src/proto_alpha/lib_protocol/saturation_repr.mli b/src/proto_alpha/lib_protocol/saturation_repr.mli index d7ce4484590d..234bd94ffbcc 100644 --- a/src/proto_alpha/lib_protocol/saturation_repr.mli +++ b/src/proto_alpha/lib_protocol/saturation_repr.mli @@ -150,6 +150,13 @@ val of_int_opt : int -> may_saturate t option and [None] otherwise. *) val of_z_opt : Z.t -> may_saturate t option +(** [saturate_if_undef o] is [saturated] if [o] is [None] and [x] if [o = Some + x]. *) +val saturate_if_undef : may_saturate t option -> may_saturate t + +(** [safe_int x] is [of_int_opt x |> saturate_if_undef]. *) +val safe_int : int -> may_saturate t + (** [to_z z] is [Z.of_int]. *) val to_z : _ t -> Z.t diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index 95916b1367bd..6f0966a21513 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -28,6 +28,7 @@ open Alpha_context open Script open Script_typed_ir open Script_ir_translator +module S = Saturation_repr (* ---- Run-time errors -----------------------------------------------------*) @@ -775,8 +776,10 @@ let rec step_bounded : (* The cost for this fold_left has been paid upfront *) let total_length = List.fold_left - (fun acc s -> Z.add acc (Z.of_int (String.length s))) - Z.zero + (fun acc s -> + let len = S.of_int_opt (String.length s) |> S.saturate_if_undef in + S.add acc len) + (S.zero |> S.may_saturate) ss.elements in Gas.consume ctxt (Interp_costs.concat_string total_length) @@ -802,8 +805,10 @@ let rec step_bounded : (* The cost for this fold_left has been paid upfront *) let total_length = List.fold_left - (fun acc s -> Z.add acc (Z.of_int (Bytes.length s))) - Z.zero + (fun acc s -> + let len = S.of_int_opt (Bytes.length s) |> S.saturate_if_undef in + S.add acc len) + (S.zero |> S.may_saturate) ss.elements in Gas.consume ctxt (Interp_costs.concat_string total_length) diff --git a/src/proto_alpha/lib_protocol/script_repr.ml b/src/proto_alpha/lib_protocol/script_repr.ml index c9c74ede8469..4ad62a4f0e24 100644 --- a/src/proto_alpha/lib_protocol/script_repr.ml +++ b/src/proto_alpha/lib_protocol/script_repr.ml @@ -98,7 +98,11 @@ let seq_node_size_nonrec args = let n_args = List.length args in seq_node_size_nonrec_of_length n_args -let convert_pair (i1, i2) = (Z.of_int i1, Z.of_int i2) +module S = Saturation_repr + +let safe_int x = S.of_int_opt x |> S.saturate_if_undef + +let convert_pair (i1, i2) = (safe_int i1, safe_int i2) let rec node_size node = let open Micheline in @@ -113,14 +117,14 @@ let rec node_size node = List.fold_left (fun (blocks, words) node -> let (nblocks, nwords) = node_size node in - (Z.add blocks nblocks, Z.add words nwords)) + (S.add blocks nblocks, S.add words nwords)) (convert_pair (prim_node_size_nonrec args annot)) args | Seq (_, args) -> List.fold_left (fun (blocks, words) node -> let (nblocks, nwords) = node_size node in - (Z.add blocks nblocks, Z.add words nwords)) + (S.add blocks nblocks, S.add words nwords)) (convert_pair (seq_node_size_nonrec args)) args @@ -132,7 +136,7 @@ let traversal_cost node = let cost_of_size (blocks, words) = let open Gas_limit_repr in - (Compare.Z.max Z.zero (Z.sub blocks Z.one) *@ alloc_cost Z.zero) + (S.max S.zero (S.sub blocks (safe_int 1)) *@ alloc_cost S.zero) +@ alloc_cost words +@ step_cost blocks let cost_of_size_int pair = cost_of_size (convert_pair pair) @@ -255,7 +259,7 @@ and micheline_nodes_list subterms acc k = let micheline_nodes node = micheline_nodes node 0 (fun x -> x) -let cost_MICHELINE_STRIP_LOCATIONS size = Z.mul (Z.of_int size) (Z.of_int 100) +let cost_MICHELINE_STRIP_LOCATIONS size = S.mul (safe_int size) (safe_int 100) let strip_locations_cost node = let nodes = micheline_nodes node in diff --git a/src/proto_alpha/lib_protocol/storage_costs.ml b/src/proto_alpha/lib_protocol/storage_costs.ml index f2d14564babe..dae9e12456fe 100644 --- a/src/proto_alpha/lib_protocol/storage_costs.ml +++ b/src/proto_alpha/lib_protocol/storage_costs.ml @@ -28,14 +28,16 @@ cost(path_length, read_bytes) = 200_000 + 5000 * path_length + 2 * read_bytes *) let read_access ~path_length ~read_bytes = - let base_cost = Z.of_int (200_000 + (5000 * path_length)) in + let open Saturation_repr in + let base_cost = safe_int (200_000 + (5000 * path_length)) in Gas_limit_repr.atomic_step_cost - (Z.add base_cost (Z.mul (Z.of_int 2) (Z.of_int read_bytes))) + (add base_cost (mul (safe_int 2) (safe_int read_bytes))) (* The model for write accesses is the following: cost(written_bytes) = 200_000 + 4 * written_bytes *) let write_access ~written_bytes = + let open Saturation_repr in Gas_limit_repr.atomic_step_cost - (Z.add (Z.of_int 200_000) (Z.mul (Z.of_int 4) (Z.of_int written_bytes))) + (add (safe_int 200_000) (mul (safe_int 4) (safe_int written_bytes))) diff --git a/src/proto_alpha/lib_protocol/test/test_gas_costs.ml b/src/proto_alpha/lib_protocol/test/test_gas_costs.ml index 3b14562a32e0..c0c46af4e7a0 100644 --- a/src/proto_alpha/lib_protocol/test/test_gas_costs.ml +++ b/src/proto_alpha/lib_protocol/test/test_gas_costs.ml @@ -34,6 +34,7 @@ open Protocol open Script_ir_translator +module S = Saturation_repr let dummy_list = list_cons 42 list_empty @@ -145,8 +146,8 @@ let all_interpreter_costs = ("compare", compare Script_typed_ir.(Int_key None) forty_two forty_two); ( "concat_string_precheck", concat_string_precheck (list_cons "42" list_empty) ); - ("concat_string", concat_string (Z.of_int 42)); - ("concat_bytes", concat_bytes (Z.of_int 42)); + ("concat_string", concat_string (S.safe_int 42)); + ("concat_bytes", concat_bytes (S.safe_int 42)); ("exec", exec); ("apply", apply); ("lambda", lambda); @@ -228,17 +229,17 @@ let all_io_costs = ("write_access 1", write_access ~written_bytes:1) ] (* Here we're using knowledge of the internal representation of costs to - cast them to Z ... *) -let cast_cost_to_z (c : Alpha_context.Gas.cost) : Z.t = + cast them to S ... *) +let cast_cost_to_s (c : Alpha_context.Gas.cost) : _ S.t = Data_encoding.Binary.to_bytes_exn Alpha_context.Gas.cost_encoding c - |> Data_encoding.Binary.of_bytes_exn Data_encoding.z + |> Data_encoding.Binary.of_bytes_exn S.n_encoding (** Checks that all costs are positive values. *) let test_cost_reprs_are_all_positive list () = List.iter_es (fun (cost_name, cost) -> - if Z.gt cost Z.zero then return_unit - else if Z.equal cost Z.zero && List.mem cost_name free then return_unit + if S.(cost > S.zero) then return_unit + else if S.equal cost S.zero && List.mem cost_name free then return_unit else fail (Exn @@ -248,7 +249,7 @@ let test_cost_reprs_are_all_positive list () = (** Checks that all costs are positive values. *) let test_costs_are_all_positive list () = let list = - List.map (fun (cost_name, cost) -> (cost_name, cast_cost_to_z cost)) list + List.map (fun (cost_name, cost) -> (cost_name, cast_cost_to_s cost)) list in test_cost_reprs_are_all_positive list () diff --git a/src/proto_alpha/lib_protocol/test/test_gas_levels.ml b/src/proto_alpha/lib_protocol/test/test_gas_levels.ml index 586aa2b02293..2170ffdd50bf 100644 --- a/src/proto_alpha/lib_protocol/test/test_gas_levels.ml +++ b/src/proto_alpha/lib_protocol/test/test_gas_levels.ml @@ -32,6 +32,7 @@ open Protocol open Raw_context +module S = Saturation_repr (* This value is supposed to be larger than the block gas level limit but not saturated. *) @@ -60,7 +61,7 @@ let test_detect_gas_exhaustion_in_fresh_context () = dummy_context () >>=? fun context -> fail_unless - (consume_gas context (Z.of_int opg) |> succeed) + (consume_gas context (S.safe_int opg) |> succeed) (err "In a fresh context, gas consumption is unlimited.") let make_context initial_operation_gas = @@ -74,14 +75,14 @@ let test_detect_gas_exhaustion_when_operation_gas_hits_zero () = make_context 10 >>=? fun context -> fail_unless - (consume_gas context (Z.of_int opg) |> failed) + (consume_gas context (S.safe_int opg) |> failed) (err "Fail when consuming more than the remaining operation gas.") let test_detect_gas_exhaustion_when_block_gas_hits_zero () = make_context opg >>=? fun context -> fail_unless - (consume_gas context (Z.of_int opg) |> failed) + (consume_gas context (S.safe_int opg) |> failed) (err "Fail when consuming more than the remaining block gas.") let monitor initial_operation_level gas_level expectation () = @@ -89,7 +90,7 @@ let monitor initial_operation_level gas_level expectation () = make_context initial_operation_level >>=? fun context -> fail_unless - ( match consume_gas context (Z.of_int 10000) (* in milligas. *) with + ( match consume_gas context (S.safe_int 10000) (* in milligas. *) with | Ok context -> let remaining = gas_level context in remaining = integral_of_int_exn expectation diff --git a/src/proto_alpha/lib_protocol/test/test_gas_properties.ml b/src/proto_alpha/lib_protocol/test/test_gas_properties.ml index 66ee2b10e2b7..ae72c19d4d67 100644 --- a/src/proto_alpha/lib_protocol/test/test_gas_properties.ml +++ b/src/proto_alpha/lib_protocol/test/test_gas_properties.ml @@ -31,6 +31,7 @@ *) open Protocol +module S = Saturation_repr type cost_kind = | Atomic_step @@ -66,19 +67,19 @@ let random_cost_of_kind (cost_kind : cost_kind) = let rand = Random.int 1000 in match cost_kind with | Atomic_step -> - atomic_step_cost (Z.of_int rand) + atomic_step_cost (S.safe_int rand) | Step -> - step_cost (Z.of_int rand) + step_cost (S.safe_int rand) | Alloc -> - alloc_cost (Z.of_int rand) + alloc_cost (S.safe_int rand) | Alloc_bytes -> alloc_bytes_cost rand | Alloc_mbytes -> alloc_mbytes_cost rand | Read_bytes -> - read_bytes_cost (Z.of_int rand) + read_bytes_cost rand | Write_bytes -> - write_bytes_cost (Z.of_int rand) + write_bytes_cost rand let random_cost () = random_cost_of_kind (random_cost_kind ()) diff --git a/src/proto_alpha/lib_protocol/test/test_script_gas.ml b/src/proto_alpha/lib_protocol/test/test_script_gas.ml index 52504e4231b4..c0c46933e73f 100644 --- a/src/proto_alpha/lib_protocol/test/test_script_gas.ml +++ b/src/proto_alpha/lib_protocol/test/test_script_gas.ml @@ -32,6 +32,7 @@ *) open Protocol +module S = Saturation_repr module Tested_terms () = struct open Micheline @@ -106,14 +107,14 @@ module Tested_terms () = struct List.iter2_e ~when_different_lengths: (TzTrace.make @@ Exn (Failure "differently sized cost lists")) - (fun min full -> - if Z.leq min full then ok_unit + (fun smin full -> + if S.(smin <= full) then ok_unit else generic_error "Script_repr: inconsistent costs %a vs %a@." - Z.pp_print - min - Z.pp_print + S.pp + smin + S.pp full) minimal_costs full_costs -- GitLab From 921091537135e9ab96596666dda6ec4e73737ea8 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Mon, 28 Dec 2020 14:14:15 +0100 Subject: [PATCH 02/23] Proto: Rename Z_syntax to S_syntax in cost model implementation Signed-off-by: Yann Regis-Gianas --- .../lib_protocol/michelson_v1_gas.ml | 48 +++++++++---------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml index 13bb0577fab7..4a10fb27e924 100644 --- a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml +++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml @@ -30,7 +30,7 @@ open Gas module S = Saturation_repr module Cost_of = struct - module Z_syntax = struct + module S_syntax = struct (* This is a good enough approximation. S.numbits 0 = 0 *) let log2 x = match S.of_int_opt (1 + Z.numbits (S.to_z x)) with @@ -170,7 +170,7 @@ module Cost_of = struct (* model N_Blake2b *) (* Approximating 1.366428 x term *) let cost_N_Blake2b size = - let open Z_syntax in + let open S_syntax in let size = safe_int size in safe_int 500 + (size + (size lsr 2)) @@ -183,21 +183,21 @@ module Cost_of = struct (* model N_Check_signature_ed25519 *) (* Approximating 1.372685 x term *) let cost_N_Check_signature_ed25519 size = - let open Z_syntax in + let open S_syntax in let size = safe_int size in safe_const 270_000 + (size + (size lsr 2)) (* model N_Check_signature_p256 *) (* Approximating 1.385771 x term *) let cost_N_Check_signature_p256 size = - let open Z_syntax in + let open S_syntax in let size = safe_int size in safe_const 600_000 + (size + (size lsr 2) + (size lsr 3)) (* model N_Check_signature_secp256k1 *) (* Approximating 1.372411 x term *) let cost_N_Check_signature_secp256k1 size = - let open Z_syntax in + let open S_syntax in let size = safe_int size in safe_const 60_000 + (size + (size lsr 2)) @@ -250,7 +250,7 @@ module Cost_of = struct (* model N_Concat_string_pair *) (* Approximating 0.068808 x term *) let cost_N_Concat_string_pair size1 size2 = - let open Z_syntax in + let open S_syntax in let v0 = safe_int size1 + safe_int size2 in safe_int 80 + (v0 lsr 4) @@ -300,7 +300,7 @@ module Cost_of = struct let q = size1 - size2 in if Compare.Int.(q < 0) then safe_const 300 else - let open Z_syntax in + let open S_syntax in let v0 = safe_int q * safe_int size2 in safe_const 300 + (v0 lsr 10) + (v0 lsr 11) + (v0 lsr 13) @@ -340,7 +340,7 @@ module Cost_of = struct (* model N_Keccak *) let cost_N_Keccak size = - let open Z_syntax in + let open S_syntax in safe_const 1_400 + (safe_const 30 * safe_int size) (* model N_Left *) @@ -348,12 +348,12 @@ module Cost_of = struct (* model N_List_iter *) let cost_N_List_iter size = - let open Z_syntax in + let open S_syntax in safe_const 500 + (safe_const 7 * safe_int size) (* model N_List_map *) let cost_N_List_map size = - let open Z_syntax in + let open S_syntax in safe_const 500 + (safe_const 12 * safe_int size) (* model N_List_size *) @@ -376,24 +376,24 @@ module Cost_of = struct (* model N_Map_get *) (* Approximating 0.057548 x term *) let cost_N_Map_get size1 size2 = - let open Z_syntax in + let open S_syntax in let v0 = size1 * log2 size2 in safe_const 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) (* model N_Map_iter *) let cost_N_Map_iter size = - let open Z_syntax in + let open S_syntax in safe_const 80 + (safe_const 40 * safe_int size) (* model N_Map_map *) let cost_N_Map_map size = - let open Z_syntax in + let open S_syntax in safe_const 80 + (safe_const 761 * safe_int size) (* model N_Map_mem *) (* Approximating 0.058563 x term *) let cost_N_Map_mem size1 size2 = - let open Z_syntax in + let open S_syntax in let v0 = size1 * log2 size2 in safe_const 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) @@ -403,7 +403,7 @@ module Cost_of = struct (* model N_Map_update *) (* Approximating 0.119968 x term *) let cost_N_Map_update size1 size2 = - let open Z_syntax in + let open S_syntax in let v0 = size1 * log2 size2 in safe_const 80 + (v0 lsr 4) + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) @@ -431,7 +431,7 @@ module Cost_of = struct (* model N_Mul_intint *) let cost_N_Mul_intint size1 size2 = - let open Z_syntax in + let open S_syntax in let a = S.add (safe_int size1) (safe_int size2) in safe_const 80 + (a * log2 a) @@ -494,13 +494,13 @@ module Cost_of = struct (* model N_Set_iter *) let cost_N_Set_iter size = - let open Z_syntax in + let open S_syntax in safe_const 80 + (safe_const 36 * safe_int size) (* model N_Set_mem *) (* Approximating 0.059410 x term *) let cost_N_Set_mem size1 size2 = - let open Z_syntax in + let open S_syntax in let v0 = size1 * log2 (safe_int size2) in safe_const 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) + (v0 lsr 8) @@ -510,23 +510,23 @@ module Cost_of = struct (* model N_Set_update *) (* Approximating 0.126260 x term *) let cost_N_Set_update size1 size2 = - let open Z_syntax in + let open S_syntax in let v0 = size1 * log2 (safe_int size2) in safe_const 80 + (v0 lsr 3) (* model N_Sha256 *) let cost_N_Sha256 size = - let open Z_syntax in + let open S_syntax in safe_const 500 + (safe_const 5 * safe_int size) (* model N_Sha3 *) let cost_N_Sha3 size = - let open Z_syntax in + let open S_syntax in safe_const 1_400 + (safe_const 32 * safe_int size) (* model N_Sha512 *) let cost_N_Sha512 size = - let open Z_syntax in + let open S_syntax in safe_const 500 + (safe_const 3 * safe_int size) (* model N_Slice_string *) @@ -723,7 +723,7 @@ module Cost_of = struct (* model CHECK_PRINTABLE *) let cost_CHECK_PRINTABLE size = - let open Z_syntax in + let open S_syntax in safe_const 14 + (safe_const 10 * safe_int size) (* model MERGE_TYPES @@ -1035,7 +1035,7 @@ module Cost_of = struct let dupn n = atomic_step_cost (cost_N_DupN n) let sapling_verify_update ~inputs ~outputs = - let open Z_syntax in + let open S_syntax in atomic_step_cost ( safe_const 85_000 + (safe_int inputs * safe_int 4) -- GitLab From d5c09b33c2fc1aacfdd3e1157ee99c08747d966a Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Mon, 28 Dec 2020 14:48:59 +0100 Subject: [PATCH 03/23] Proto: Export and use `shift_right` for saturation arith Signed-off-by: Yann Regis-Gianas --- .../lib_protocol/michelson_v1_gas.ml | 9 +- .../lib_protocol/saturation_repr.ml | 4 + .../lib_protocol/saturation_repr.mli | 4 + src/proto_alpha/lib_protocol/script_repr.ml | 3 +- .../lib_protocol/test/saturation.ml | 109 ++++++++++++++++++ 5 files changed, 121 insertions(+), 8 deletions(-) create mode 100644 src/proto_alpha/lib_protocol/test/saturation.ml diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml index 4a10fb27e924..cfbde0da7b18 100644 --- a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml +++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml @@ -43,12 +43,7 @@ module Cost_of = struct let ( * ) = S.mul - let ( lsr ) (x : _ S.t) y = - match (x |> S.to_int) lsr y |> S.of_int_opt with - | None -> - S.saturated - | Some x -> - x + let ( lsr ) = S.shift_right end let z_bytes (z : Z.t) = @@ -437,7 +432,7 @@ module Cost_of = struct (* model N_Mul_teznat *) let cost_N_Mul_teznat size = - let open Z_syntax in + let open S_syntax in safe_const 200 + (safe_const 133 * safe_int size) (* model N_Neg_bls12_381_fr *) diff --git a/src/proto_alpha/lib_protocol/saturation_repr.ml b/src/proto_alpha/lib_protocol/saturation_repr.ml index 1ecfaf90c160..7db5dcd4c915 100644 --- a/src/proto_alpha/lib_protocol/saturation_repr.ml +++ b/src/proto_alpha/lib_protocol/saturation_repr.ml @@ -78,6 +78,10 @@ let small_enough z = let mul_safe x = if small_enough x then Some x else None +(* If [x] is positive, shifting to the right will produce a number + which is positive and is less than [x]. *) +let shift_right x y = (x :> int) lsr y + let mul x y = (* assert (x >= 0 && y >= 0); *) match x with diff --git a/src/proto_alpha/lib_protocol/saturation_repr.mli b/src/proto_alpha/lib_protocol/saturation_repr.mli index 234bd94ffbcc..1618e2e31dfc 100644 --- a/src/proto_alpha/lib_protocol/saturation_repr.mli +++ b/src/proto_alpha/lib_protocol/saturation_repr.mli @@ -96,6 +96,10 @@ val max : 'a t -> 'a t -> 'a t val compare : 'a t -> 'b t -> int +(** [shift_right x y] behaves like a logical shift of [x] by [y] bits + to the right. [y] must be between 0 and 63. *) +val shift_right : 'a t -> int -> 'a t + (** [mul x y] behaves like multiplication between native integers as long as its result stay below [saturated]. Otherwise, [mul] returns [saturated]. *) diff --git a/src/proto_alpha/lib_protocol/script_repr.ml b/src/proto_alpha/lib_protocol/script_repr.ml index 4ad62a4f0e24..0c400464a2de 100644 --- a/src/proto_alpha/lib_protocol/script_repr.ml +++ b/src/proto_alpha/lib_protocol/script_repr.ml @@ -136,7 +136,8 @@ let traversal_cost node = let cost_of_size (blocks, words) = let open Gas_limit_repr in - (S.max S.zero (S.sub blocks (safe_int 1)) *@ alloc_cost S.zero) + S.max (S.zero |> S.may_saturate) (S.sub blocks (safe_int 1)) + *@ alloc_cost S.zero +@ alloc_cost words +@ step_cost blocks let cost_of_size_int pair = cost_of_size (convert_pair pair) diff --git a/src/proto_alpha/lib_protocol/test/saturation.ml b/src/proto_alpha/lib_protocol/test/saturation.ml new file mode 100644 index 000000000000..427c3c73cd2f --- /dev/null +++ b/src/proto_alpha/lib_protocol/test/saturation.ml @@ -0,0 +1,109 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2020 Nomadic Labs, *) +(* *) +(* Permission is hereby granted, free of charge, to any person obtaining a *) +(* copy of this software and associated documentation files (the "Software"),*) +(* to deal in the Software without restriction, including without limitation *) +(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *) +(* and/or sell copies of the Software, and to permit persons to whom the *) +(* Software is furnished to do so, subject to the following conditions: *) +(* *) +(* The above copyright notice and this permission notice shall be included *) +(* in all copies or substantial portions of the Software. *) +(* *) +(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*) +(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *) +(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *) +(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*) +(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *) +(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *) +(* DEALINGS IN THE SOFTWARE. *) +(* *) +(*****************************************************************************) + +open Protocol + +let valid (z : _ Saturation_repr.t) = + let x = z |> Saturation_repr.to_int in + x >= 0 && x < max_int + +open Saturation_repr + +exception Saturating_test_error of string + +let err x = Exn (Saturating_test_error x) + +let small_enough (z : _ t) = + Compare.Int.((z |> to_int) land 0x7fffffff80000000 = 0) + +let n = safe_int 123123 + +let m = safe_int 377337 + +let shift_right () = + fail_unless + (shift_right saturated 63 = safe_int 0) + (err "saturated lsr 63 = 0") + >>=? fun () -> + fail_unless (shift_right (safe_int 1) 63 = safe_int 0) (err "1 lsr 63 = 0") + >>=? fun () -> + fail_unless (shift_right (safe_int 1) 0 = safe_int 1) (err "1 lsr 0 = 1") + >>=? fun () -> + fail_unless (shift_right (safe_int 0) 63 = safe_int 0) (err "0 lsr 63 = 0") + +let add () = + fail_unless + (add saturated (safe_int 1) = saturated) + (err "saturated + 1 <> saturated") + >>=? fun () -> + fail_unless (add zero n = n) (err "zero + n = n") + >>=? fun () -> + fail_unless (add n zero = n) (err "n + zero = n") + >>=? fun () -> + let r = add n m in + fail_unless + (valid r && r = safe_int ((n :> int) + (m :> int))) + (err "add does not behave like + on small numbers.") + +let sub () = + fail_unless (sub zero n = zero) (err "zero - n <> zero") + >>=? fun () -> + let n = max n m and m = min n m in + let r = sub n m in + fail_unless + (valid r && r = safe_int ((n :> int) - (m :> int))) + (err "sub does not behave like - on small numbers.") + +let mul () = + fail_unless + (mul saturated saturated = saturated) + (err "saturated * saturated <> saturated") + >>=? fun () -> + fail_unless (mul zero saturated = zero) (err "zero * saturated <> zero") + >>=? fun () -> + fail_unless (mul saturated zero = zero) (err "saturated * zero <> zero") + >>=? fun () -> + let max_squared = safe_int (1 lsl 31) in + let r = mul max_squared max_squared in + fail_unless + (valid r && r = saturated) + (err "2 ^ 31 * 2 ^ 31 should be saturated") + >>=? fun () -> + let safe_squared = safe_int ((1 lsl 31) - 1) in + let r = mul safe_squared safe_squared in + fail_unless + (valid r && r <> saturated) + (err "(2 ^ 31 - 1) * (2 ^ 31 - 1) should not be saturated") + >>=? fun () -> + let r = mul n m in + fail_unless + (valid r && r = safe_int ((n |> to_int) * (m |> to_int))) + (err "mul does not behave like * on small numbers.") + +let tests = + [ Test.tztest "Shift right" `Quick shift_right; + Test.tztest "Addition" `Quick add; + Test.tztest "Subtraction" `Quick sub; + Test.tztest "Multiplication" `Quick mul ] -- GitLab From 63f89a86990fed67336fb9c76d55876d0fcce3d2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Hurlin?= Date: Thu, 14 Jan 2021 21:45:01 +0100 Subject: [PATCH 04/23] saturation: add quickcheck (fuzzing) tests --- src/proto_alpha/lib_protocol/test/dune | 12 ++- .../lib_protocol/test/saturation_fuzzing.ml | 92 +++++++++++++++++++ .../tezos-protocol-alpha-tests.opam | 1 + 3 files changed, 102 insertions(+), 3 deletions(-) create mode 100644 src/proto_alpha/lib_protocol/test/saturation_fuzzing.ml diff --git a/src/proto_alpha/lib_protocol/test/dune b/src/proto_alpha/lib_protocol/test/dune index 1f9ca1646a79..87b7e95ceff7 100644 --- a/src/proto_alpha/lib_protocol/test/dune +++ b/src/proto_alpha/lib_protocol/test/dune @@ -1,9 +1,10 @@ -(executable - (name main) +(executables + (names main saturation_fuzzing) (libraries tezos-base tezos-micheline tezos-protocol-environment alcotest-lwt + crowbar tezos-alpha-test-helpers tezos-stdlib-unix tezos-client-base @@ -43,10 +44,15 @@ (package tezos-protocol-alpha-tests) (action (run %{exe:main.exe} -v))) +(rule + (alias runtest_saturation_fuzzing) + (package tezos-protocol-alpha-tests) + (action (run %{exe:saturation_fuzzing.exe}))) + (rule (alias runtest) (package tezos-protocol-alpha-tests) - (deps (alias runtest_proto_alpha)) + (deps (alias runtest_proto_alpha) (alias runtest_saturation_fuzzing)) (action (progn))) (rule diff --git a/src/proto_alpha/lib_protocol/test/saturation_fuzzing.ml b/src/proto_alpha/lib_protocol/test/saturation_fuzzing.ml new file mode 100644 index 000000000000..1447e5ebfb2e --- /dev/null +++ b/src/proto_alpha/lib_protocol/test/saturation_fuzzing.ml @@ -0,0 +1,92 @@ +(*****************************************************************************) +(* *) +(* Open Source License *) +(* Copyright (c) 2021 Nomadic Labs, *) +(* *) +(* Permission is hereby granted, free of charge, to any person obtaining a *) +(* copy of this software and associated documentation files (the "Software"),*) +(* to deal in the Software without restriction, including without limitation *) +(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *) +(* and/or sell copies of the Software, and to permit persons to whom the *) +(* Software is furnished to do so, subject to the following conditions: *) +(* *) +(* The above copyright notice and this permission notice shall be included *) +(* in all copies or substantial portions of the Software. *) +(* *) +(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*) +(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *) +(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *) +(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*) +(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *) +(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *) +(* DEALINGS IN THE SOFTWARE. *) +(* *) +(*****************************************************************************) + +(** Testing + ------- + Component: Protocol Library + Invocation: dune build @src/proto_alpha/lib_protocol/runtest_saturation_fuzzing + Subject: Operations in Saturation_repr +*) + +open Protocol.Saturation_repr + +let gen_unsaturated = + let open Crowbar in + map [int] safe_int + +let gen_t = + let open Crowbar in + choose + [ const saturated; + gen_unsaturated; + gen_unsaturated; + gen_unsaturated; + gen_unsaturated ] + +(* Test. + * Tests that [f] commutes. + *) +let test_commutes f t1 t2 = + let fapp = f t1 t2 in + let fapp' = f t2 t1 in + Crowbar.check_eq ~pp fapp fapp' + +(* Test. + * Tests that [e] is neutral for [f]. + *) +let test_neutral f e t = + let fapp = f e t in + let fapp' = f t e in + Crowbar.check_eq ~pp fapp fapp' + +(* Test. + * Tests that [t] times [1] equals [t]. + *) +let test_mul_one t = Crowbar.check_eq ~pp (mul t @@ safe_int 1) t + +(* Test. + * Tests that [t] times [0] equals [0]. + *) +let test_mul_zero t = Crowbar.check_eq ~pp (mul t zero) (zero |> may_saturate) + +(* Test. + * Tests that [t] minus [zero] equals [t]. + *) +let test_sub_zero t = Crowbar.check_eq ~pp (sub t zero) t + +let tests = + Crowbar.add_test ~name:"add commutes" [gen_t; gen_t] (test_commutes add) ; + Crowbar.add_test ~name:"mul commutes" [gen_t; gen_t] (test_commutes mul) ; + Crowbar.add_test + ~name:"0 is neutral for add" + [gen_t] + (test_neutral add (zero |> may_saturate)) ; + Crowbar.add_test + ~name:"1 is neutral for mul" + [gen_t] + (test_neutral mul (safe_int 1)) ; + Crowbar.add_test ~name:"t * 0 = 0" [gen_t] test_mul_zero ; + Crowbar.add_test ~name:"t * 1 = t" [gen_t] test_mul_one ; + Crowbar.add_test ~name:"t - 0 = t" [gen_t] test_sub_zero diff --git a/src/proto_alpha/lib_protocol/tezos-protocol-alpha-tests.opam b/src/proto_alpha/lib_protocol/tezos-protocol-alpha-tests.opam index f8255bb04b3f..b3255b429f7a 100644 --- a/src/proto_alpha/lib_protocol/tezos-protocol-alpha-tests.opam +++ b/src/proto_alpha/lib_protocol/tezos-protocol-alpha-tests.opam @@ -10,6 +10,7 @@ depends: [ "tezos-protocol-compiler" "alcotest-lwt" { with-test & >= "1.1.0" } "astring" { with-test } + "crowbar" { with-test } "tezos-alpha-test-helpers" { with-test } "tezos-stdlib-unix" { with-test } "tezos-protocol-environment" { with-test } -- GitLab From e39b12608625ae767d3a091d04a08eb77a8f67cf Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Wed, 27 Jan 2021 08:49:33 +0100 Subject: [PATCH 05/23] Proto: Remove unused safe_fp Signed-off-by: Yann Regis-Gianas --- src/proto_alpha/lib_protocol/gas_limit_repr.ml | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.ml b/src/proto_alpha/lib_protocol/gas_limit_repr.ml index c51382460496..aa46d5ae6c06 100644 --- a/src/proto_alpha/lib_protocol/gas_limit_repr.ml +++ b/src/proto_alpha/lib_protocol/gas_limit_repr.ml @@ -141,13 +141,6 @@ module Arith = struct | None -> fatally_saturated_z x - let safe_fp x = - match of_int_opt (Z.to_int x) with - | Some int -> - int - | None -> - Saturation_repr.saturated - let sub_opt = Saturation_repr.sub_opt end -- GitLab From 880fb990cf80d330c2ac2c621e884b24b8c72763 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Wed, 27 Jan 2021 08:53:59 +0100 Subject: [PATCH 06/23] Proto: Remove trailing multiple definitions of safe_int Signed-off-by: Yann Regis-Gianas --- .../lib_protocol/gas_limit_repr.ml | 13 +- .../lib_protocol/michelson_v1_gas.ml | 143 +++++++++--------- src/proto_alpha/lib_protocol/script_repr.ml | 9 +- 3 files changed, 80 insertions(+), 85 deletions(-) diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.ml b/src/proto_alpha/lib_protocol/gas_limit_repr.ml index aa46d5ae6c06..7170989b2293 100644 --- a/src/proto_alpha/lib_protocol/gas_limit_repr.ml +++ b/src/proto_alpha/lib_protocol/gas_limit_repr.ml @@ -37,13 +37,6 @@ let safe_const x = | Some x -> x -let safe_int x = - match Saturation_repr.(of_int_opt x) with - | None -> - Saturation_repr.saturated - | Some x -> - x - let scaling_factor = safe_const 1000 module Arith = struct @@ -213,10 +206,12 @@ let step_cost n = S.mul step_weight n let free = S.zero |> S.may_saturate let read_bytes_cost n = - S.add read_base_weight (S.mul byte_read_weight (safe_int n)) + S.add read_base_weight (S.mul byte_read_weight (Saturation_repr.safe_int n)) let write_bytes_cost n = - S.add write_base_weight (S.mul byte_written_weight (safe_int n)) + S.add + write_base_weight + (S.mul byte_written_weight (Saturation_repr.safe_int n)) let ( +@ ) x y = S.add x y diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml index cfbde0da7b18..b8a1cfebfa88 100644 --- a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml +++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml @@ -66,8 +66,6 @@ module Cost_of = struct | Some x -> x - let safe_int x = S.of_int_opt x |> S.saturate_if_undef - let int_bytes (z : 'a Script_int.num) = z_bytes (Script_int.to_zint z) let timestamp_bytes (t : Script_timestamp.t) = @@ -85,23 +83,23 @@ module Cost_of = struct | (Never_key _, _) -> . | (Int_key _, _) -> - safe_int @@ int_bytes v + S.safe_int @@ int_bytes v | (Nat_key _, _) -> - safe_int @@ int_bytes v + S.safe_int @@ int_bytes v | (Signature_key _, _) -> safe_const Signature.size | (String_key _, _) -> - safe_int @@ String.length v + S.safe_int @@ String.length v | (Bytes_key _, _) -> - safe_int @@ Bytes.length v + S.safe_int @@ Bytes.length v | (Bool_key _, _) -> safe_const 8 | (Key_hash_key _, _) -> safe_const Signature.Public_key_hash.size | (Key_key _, k) -> - safe_int @@ Signature.Public_key.size k + S.safe_int @@ Signature.Public_key.size k | (Timestamp_key _, _) -> - safe_int @@ timestamp_bytes v + S.safe_int @@ timestamp_bytes v | (Address_key _, _) -> safe_const Signature.Public_key_hash.size | (Mutez_key _, _) -> @@ -130,7 +128,7 @@ module Cost_of = struct (* model N_Abs_int *) (* Approximating 0.068306 x term *) - let cost_N_Abs_int size = safe_int @@ (80 + (size lsr 4)) + let cost_N_Abs_int size = S.safe_int @@ (80 + (size lsr 4)) (* model N_Add_bls12_381_fr *) @@ -148,7 +146,7 @@ module Cost_of = struct (* Approximating 0.082158 x term *) let cost_N_Add_intint size1 size2 = let v0 = Compare.Int.max size1 size2 in - safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) + S.safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) (* model N_Add_tez *) let cost_N_Add_tez = safe_const 100 @@ -160,14 +158,14 @@ module Cost_of = struct (* Approximating 0.079325 x term *) let cost_N_And_nat size1 size2 = let v0 = Compare.Int.min size1 size2 in - safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) + S.safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) (* model N_Blake2b *) (* Approximating 1.366428 x term *) let cost_N_Blake2b size = let open S_syntax in - let size = safe_int size in - safe_int 500 + (size + (size lsr 2)) + let size = S.safe_int size in + S.safe_int 500 + (size + (size lsr 2)) (* model N_Car *) let cost_N_Car = safe_const 80 @@ -179,75 +177,75 @@ module Cost_of = struct (* Approximating 1.372685 x term *) let cost_N_Check_signature_ed25519 size = let open S_syntax in - let size = safe_int size in + let size = S.safe_int size in safe_const 270_000 + (size + (size lsr 2)) (* model N_Check_signature_p256 *) (* Approximating 1.385771 x term *) let cost_N_Check_signature_p256 size = let open S_syntax in - let size = safe_int size in + let size = S.safe_int size in safe_const 600_000 + (size + (size lsr 2) + (size lsr 3)) (* model N_Check_signature_secp256k1 *) (* Approximating 1.372411 x term *) let cost_N_Check_signature_secp256k1 size = let open S_syntax in - let size = safe_int size in + let size = S.safe_int size in safe_const 60_000 + (size + (size lsr 2)) (* model N_Comb *) (* Approximating 3.275337 x term *) - let cost_N_Comb size = safe_int (80 + ((3 * size) + (size lsr 2))) + let cost_N_Comb size = S.safe_int (80 + ((3 * size) + (size lsr 2))) (* model N_Comb_get *) (* Approximating 0.553178 x term *) - let cost_N_Comb_get size = safe_int (80 + ((size lsr 1) + (size lsr 4))) + let cost_N_Comb_get size = S.safe_int (80 + ((size lsr 1) + (size lsr 4))) (* model N_Comb_set *) (* Approximating 1.282976 x term *) - let cost_N_Comb_set size = safe_int (80 + (size + (size lsr 2))) + let cost_N_Comb_set size = S.safe_int (80 + (size + (size lsr 2))) (* model N_Compare_address *) let cost_N_Compare_address size1 size2 = - safe_int (80 + (2 * Compare.Int.min size1 size2)) + S.safe_int (80 + (2 * Compare.Int.min size1 size2)) (* model N_Compare_bool *) let cost_N_Compare_bool size1 size2 = - safe_int (80 + (128 * Compare.Int.min size1 size2)) + S.safe_int (80 + (128 * Compare.Int.min size1 size2)) (* model N_Compare_int *) (* Approximating 0.073657 x term *) let cost_N_Compare_int size1 size2 = let v0 = Compare.Int.min size1 size2 in - safe_int (150 + ((v0 lsr 4) + (v0 lsr 7))) + S.safe_int (150 + ((v0 lsr 4) + (v0 lsr 7))) (* model N_Compare_key_hash *) let cost_N_Compare_key_hash size1 size2 = - safe_int (80 + (2 * Compare.Int.min size1 size2)) + S.safe_int (80 + (2 * Compare.Int.min size1 size2)) (* model N_Compare_mutez *) let cost_N_Compare_mutez size1 size2 = - safe_int (13 * Compare.Int.min size1 size2) + S.safe_int (13 * Compare.Int.min size1 size2) (* model N_Compare_string *) (* Approximating 0.039389 x term *) let cost_N_Compare_string size1 size2 = let v0 = Compare.Int.min size1 size2 in - safe_int (120 + ((v0 lsr 5) + (v0 lsr 7))) + S.safe_int (120 + ((v0 lsr 5) + (v0 lsr 7))) (* model N_Compare_timestamp *) (* Approximating 0.072483 x term *) let cost_N_Compare_timestamp size1 size2 = let v0 = Compare.Int.min size1 size2 in - safe_int (140 + ((v0 lsr 4) + (v0 lsr 7))) + S.safe_int (140 + ((v0 lsr 4) + (v0 lsr 7))) (* model N_Concat_string_pair *) (* Approximating 0.068808 x term *) let cost_N_Concat_string_pair size1 size2 = let open S_syntax in - let v0 = safe_int size1 + safe_int size2 in - safe_int 80 + (v0 lsr 4) + let v0 = S.safe_int size1 + S.safe_int size2 in + S.safe_int 80 + (v0 lsr 4) (* model N_Cons_list *) let cost_N_Cons_list = safe_const 80 @@ -265,29 +263,29 @@ module Cost_of = struct let cost_N_Const = safe_const 80 (* model N_Dig *) - let cost_N_Dig size = safe_int (100 + (4 * size)) + let cost_N_Dig size = S.safe_int (100 + (4 * size)) (* model N_Dip *) let cost_N_Dip = safe_const 100 (* model N_DipN *) - let cost_N_DipN size = safe_int (100 + (4 * size)) + let cost_N_DipN size = S.safe_int (100 + (4 * size)) (* model N_Drop *) let cost_N_Drop = safe_const 80 (* model N_DropN *) - let cost_N_DropN size = safe_int (100 + (4 * size)) + let cost_N_DropN size = S.safe_int (100 + (4 * size)) (* model N_Dug *) - let cost_N_Dug size = safe_int (100 + (4 * size)) + let cost_N_Dug size = S.safe_int (100 + (4 * size)) (* model N_Dup *) - let cost_N_Dup = safe_int 80 + let cost_N_Dup = S.safe_int 80 (* model N_DupN *) (* Approximating 1.299969 x term *) - let cost_N_DupN size = safe_int (60 + size + (size lsr 2)) + let cost_N_DupN size = S.safe_int (60 + size + (size lsr 2)) (* model N_Ediv_natnat *) (* Approximating 0.001599 x term *) @@ -296,7 +294,7 @@ module Cost_of = struct if Compare.Int.(q < 0) then safe_const 300 else let open S_syntax in - let v0 = safe_int q * safe_int size2 in + let v0 = S.safe_int q * S.safe_int size2 in safe_const 300 + (v0 lsr 10) + (v0 lsr 11) + (v0 lsr 13) (* model N_Ediv_tez *) @@ -336,7 +334,7 @@ module Cost_of = struct (* model N_Keccak *) let cost_N_Keccak size = let open S_syntax in - safe_const 1_400 + (safe_const 30 * safe_int size) + safe_const 1_400 + (safe_const 30 * S.safe_int size) (* model N_Left *) let cost_N_Left = safe_const 80 @@ -344,12 +342,12 @@ module Cost_of = struct (* model N_List_iter *) let cost_N_List_iter size = let open S_syntax in - safe_const 500 + (safe_const 7 * safe_int size) + safe_const 500 + (safe_const 7 * S.safe_int size) (* model N_List_map *) let cost_N_List_map size = let open S_syntax in - safe_const 500 + (safe_const 12 * safe_int size) + safe_const 500 + (safe_const 12 * S.safe_int size) (* model N_List_size *) let cost_N_List_size = safe_const 80 @@ -362,11 +360,11 @@ module Cost_of = struct (* model N_Lsl_nat *) (* Approximating 0.129443 x term *) - let cost_N_Lsl_nat size = safe_int (150 + (size lsr 3)) + let cost_N_Lsl_nat size = S.safe_int (150 + (size lsr 3)) (* model N_Lsr_nat *) (* Approximating 0.129435 x term *) - let cost_N_Lsr_nat size = safe_int (150 + (size lsr 3)) + let cost_N_Lsr_nat size = S.safe_int (150 + (size lsr 3)) (* model N_Map_get *) (* Approximating 0.057548 x term *) @@ -378,12 +376,12 @@ module Cost_of = struct (* model N_Map_iter *) let cost_N_Map_iter size = let open S_syntax in - safe_const 80 + (safe_const 40 * safe_int size) + safe_const 80 + (safe_const 40 * S.safe_int size) (* model N_Map_map *) let cost_N_Map_map size = let open S_syntax in - safe_const 80 + (safe_const 761 * safe_int size) + safe_const 80 + (safe_const 761 * S.safe_int size) (* model N_Map_mem *) (* Approximating 0.058563 x term *) @@ -427,13 +425,13 @@ module Cost_of = struct (* model N_Mul_intint *) let cost_N_Mul_intint size1 size2 = let open S_syntax in - let a = S.add (safe_int size1) (safe_int size2) in + let a = S.add (S.safe_int size1) (S.safe_int size2) in safe_const 80 + (a * log2 a) (* model N_Mul_teznat *) let cost_N_Mul_teznat size = let open S_syntax in - safe_const 200 + (safe_const 133 * safe_int size) + safe_const 200 + (safe_const 133 * S.safe_int size) (* model N_Neg_bls12_381_fr *) @@ -449,7 +447,7 @@ module Cost_of = struct (* model N_Neg_int *) (* Approximating 0.068419 x term *) - let cost_N_Neg_int size = safe_int (80 + (size lsr 4)) + let cost_N_Neg_int size = S.safe_int (80 + (size lsr 4)) (* model N_Neq *) let cost_N_Neq = safe_const 80 @@ -465,7 +463,7 @@ module Cost_of = struct (* model N_Not_int *) (* Approximating 0.076564 x term *) - let cost_N_Not_int size = safe_int (55 + ((size lsr 4) + (size lsr 7))) + let cost_N_Not_int size = S.safe_int (55 + ((size lsr 4) + (size lsr 7))) (* model N_Or *) let cost_N_Or = safe_const 90 @@ -474,12 +472,14 @@ module Cost_of = struct (* Approximating 0.078718 x term *) let cost_N_Or_nat size1 size2 = let v0 = Compare.Int.max size1 size2 in - safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) + S.safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) (* model N_Pairing_check_bls12_381 *) let cost_N_Pairing_check_bls12_381 size = - S.add (safe_const 1_550_000) (S.mul (safe_const 510_000) (safe_int size)) + S.add + (safe_const 1_550_000) + (S.mul (safe_const 510_000) (S.safe_int size)) (* model N_Right *) let cost_N_Right = safe_const 80 @@ -490,13 +490,13 @@ module Cost_of = struct (* model N_Set_iter *) let cost_N_Set_iter size = let open S_syntax in - safe_const 80 + (safe_const 36 * safe_int size) + safe_const 80 + (safe_const 36 * S.safe_int size) (* model N_Set_mem *) (* Approximating 0.059410 x term *) let cost_N_Set_mem size1 size2 = let open S_syntax in - let v0 = size1 * log2 (safe_int size2) in + let v0 = size1 * log2 (S.safe_int size2) in safe_const 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) + (v0 lsr 8) (* model N_Set_size *) @@ -506,27 +506,27 @@ module Cost_of = struct (* Approximating 0.126260 x term *) let cost_N_Set_update size1 size2 = let open S_syntax in - let v0 = size1 * log2 (safe_int size2) in + let v0 = size1 * log2 (S.safe_int size2) in safe_const 80 + (v0 lsr 3) (* model N_Sha256 *) let cost_N_Sha256 size = let open S_syntax in - safe_const 500 + (safe_const 5 * safe_int size) + safe_const 500 + (safe_const 5 * S.safe_int size) (* model N_Sha3 *) let cost_N_Sha3 size = let open S_syntax in - safe_const 1_400 + (safe_const 32 * safe_int size) + safe_const 1_400 + (safe_const 32 * S.safe_int size) (* model N_Sha512 *) let cost_N_Sha512 size = let open S_syntax in - safe_const 500 + (safe_const 3 * safe_int size) + safe_const 500 + (safe_const 3 * S.safe_int size) (* model N_Slice_string *) (* Approximating 0.067048 x term *) - let cost_N_Slice_string size = safe_int (80 + (size lsr 4)) + let cost_N_Slice_string size = S.safe_int (80 + (size lsr 4)) (* model N_String_size *) let cost_N_String_size = safe_const 80 @@ -535,7 +535,7 @@ module Cost_of = struct (* Approximating 0.082399 x term *) let cost_N_Sub_int size1 size2 = let v0 = Compare.Int.max size1 size2 in - safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) + S.safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) (* model N_Sub_tez *) let cost_N_Sub_tez = safe_const 80 @@ -549,7 +549,7 @@ module Cost_of = struct (* model N_Uncomb *) (* Approximating 3.666332 x term *) let cost_N_Uncomb size = - safe_int (80 + ((3 * size) + (size lsr 1) + (size lsr 3))) + S.safe_int (80 + ((3 * size) + (size lsr 1) + (size lsr 3))) (* model N_Unpair *) let cost_N_Unpair = safe_const 80 @@ -564,7 +564,7 @@ module Cost_of = struct (* Approximating 0.078258 x term *) let cost_N_Xor_nat size1 size2 = let v0 = Compare.Int.max size1 size2 in - safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) + S.safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) (* model DECODING_BLS_FR *) @@ -719,7 +719,7 @@ module Cost_of = struct (* model CHECK_PRINTABLE *) let cost_CHECK_PRINTABLE size = let open S_syntax in - safe_const 14 + (safe_const 10 * safe_int size) + safe_const 14 + (safe_const 10 * S.safe_int size) (* model MERGE_TYPES This is the estimated cost of one iteration of merge_types, extracted @@ -833,17 +833,18 @@ module Cost_of = struct let map_mem (type k v) (elt : k) ((module Box) : (k, v) Script_typed_ir.map) = let elt_size = size_of_comparable Box.key_ty elt in - atomic_step_cost (cost_N_Map_mem elt_size (safe_int (snd Box.boxed))) + atomic_step_cost (cost_N_Map_mem elt_size (S.safe_int (snd Box.boxed))) let map_get (type k v) (elt : k) ((module Box) : (k, v) Script_typed_ir.map) = let elt_size = size_of_comparable Box.key_ty elt in - atomic_step_cost (cost_N_Map_get elt_size (safe_int (snd Box.boxed))) + atomic_step_cost (cost_N_Map_get elt_size (S.safe_int (snd Box.boxed))) let map_update (type k v) (elt : k) ((module Box) : (k, v) Script_typed_ir.map) = let elt_size = size_of_comparable Box.key_ty elt in - atomic_step_cost (cost_N_Map_update elt_size (safe_int (snd Box.boxed))) + atomic_step_cost + (cost_N_Map_update elt_size (S.safe_int (snd Box.boxed))) let map_get_and_update (type k v) (elt : k) (m : (k, v) Script_typed_ir.map) = @@ -1033,12 +1034,12 @@ module Cost_of = struct let open S_syntax in atomic_step_cost ( safe_const 85_000 - + (safe_int inputs * safe_int 4) - + (safe_int outputs * safe_int 30) ) + + (S.safe_int inputs * S.safe_int 4) + + (S.safe_int outputs * S.safe_int 30) ) (* --------------------------------------------------------------------- *) (* Semi-hand-crafted models *) - let compare_unit = atomic_step_cost (safe_int 10) + let compare_unit = atomic_step_cost (S.safe_int 10) let compare_union_tag = atomic_step_cost (safe_const 10) @@ -1160,17 +1161,17 @@ module Cost_of = struct *) let concat_string_precheck (l : 'a Script_typed_ir.boxed_list) = (* we set the precheck to be slightly more expensive than cost_N_List_iter *) - atomic_step_cost (S.mul (safe_int l.length) (safe_const 10)) + atomic_step_cost (S.mul (S.safe_int l.length) (safe_const 10)) (* This is the cost of allocating a string and blitting existing ones into it. *) let concat_string total_bytes = atomic_step_cost - S.(add (safe_int 100) (S.ediv total_bytes (safe_int 10))) + S.(add (S.safe_int 100) (S.ediv total_bytes (S.safe_int 10))) (* Same story as Concat_string. *) let concat_bytes total_bytes = atomic_step_cost - S.(add (safe_int 100) (S.ediv total_bytes (safe_int 10))) + S.(add (S.safe_int 100) (S.ediv total_bytes (S.safe_int 10))) (* Cost of additional call to logger + overhead of setting up call to [interp]. *) let exec = atomic_step_cost (safe_const 100) @@ -1242,11 +1243,11 @@ module Cost_of = struct (* We cannot instrument failed deserialization, so we take worst case fees: a set of size 1 bytes values. *) let blen = Bytes.length bytes in - let len = safe_int blen in + let len = S.safe_int blen in let d = Z.numbits (Z.of_int blen) in (len *@ alloc_mbytes_cost 1) +@ len - *@ ( safe_int d + *@ ( S.safe_int d *@ (alloc_cost (safe_const 3) +@ step_cost (safe_const 1)) ) let ticket = atomic_step_cost (safe_const 80) @@ -1380,7 +1381,7 @@ module Cost_of = struct (* Constructing proof arguments consists in a decreasing loop in the result monad, allocating at each step. We charge a reasonable overapproximation. *) let proof_argument n = - atomic_step_cost (S.mul (safe_int n) (safe_const 50)) + atomic_step_cost (S.mul (S.safe_int n) (safe_const 50)) end module Unparsing = struct diff --git a/src/proto_alpha/lib_protocol/script_repr.ml b/src/proto_alpha/lib_protocol/script_repr.ml index 0c400464a2de..dd3b4d48ac9d 100644 --- a/src/proto_alpha/lib_protocol/script_repr.ml +++ b/src/proto_alpha/lib_protocol/script_repr.ml @@ -100,9 +100,7 @@ let seq_node_size_nonrec args = module S = Saturation_repr -let safe_int x = S.of_int_opt x |> S.saturate_if_undef - -let convert_pair (i1, i2) = (safe_int i1, safe_int i2) +let convert_pair (i1, i2) = (S.safe_int i1, S.safe_int i2) let rec node_size node = let open Micheline in @@ -136,7 +134,7 @@ let traversal_cost node = let cost_of_size (blocks, words) = let open Gas_limit_repr in - S.max (S.zero |> S.may_saturate) (S.sub blocks (safe_int 1)) + S.max (S.zero |> S.may_saturate) (S.sub blocks (S.safe_int 1)) *@ alloc_cost S.zero +@ alloc_cost words +@ step_cost blocks @@ -260,7 +258,8 @@ and micheline_nodes_list subterms acc k = let micheline_nodes node = micheline_nodes node 0 (fun x -> x) -let cost_MICHELINE_STRIP_LOCATIONS size = S.mul (safe_int size) (safe_int 100) +let cost_MICHELINE_STRIP_LOCATIONS size = + S.mul (S.safe_int size) (S.safe_int 100) let strip_locations_cost node = let nodes = micheline_nodes node in -- GitLab From 610f86e70c7d3ee3befc7cf4de573b46d3c84b73 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Wed, 27 Jan 2021 08:59:08 +0100 Subject: [PATCH 07/23] Proto: Uniformize reference to Saturation_repr Signed-off-by: Yann Regis-Gianas --- .../lib_protocol/gas_limit_repr.ml | 61 +++++++++---------- 1 file changed, 29 insertions(+), 32 deletions(-) diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.ml b/src/proto_alpha/lib_protocol/gas_limit_repr.ml index 7170989b2293..460367eb4368 100644 --- a/src/proto_alpha/lib_protocol/gas_limit_repr.ml +++ b/src/proto_alpha/lib_protocol/gas_limit_repr.ml @@ -29,8 +29,10 @@ type fp_tag type integral_tag +module S = Saturation_repr + let safe_const x = - match Saturation_repr.(Option.bind (of_int_opt x) mul_safe) with + match S.(Option.bind (of_int_opt x) mul_safe) with | None -> (* because [safe_const] is always called with small enough constants. *) assert false @@ -40,7 +42,7 @@ let safe_const x = let scaling_factor = safe_const 1000 module Arith = struct - type 'a t = Saturation_repr.may_saturate Saturation_repr.t + type 'a t = S.may_saturate S.t type fp = fp_tag t @@ -48,33 +50,33 @@ module Arith = struct let scaling_factor = scaling_factor - let sub = Saturation_repr.sub + let sub = S.sub - let add = Saturation_repr.add + let add = S.add - let zero = Saturation_repr.(may_saturate zero) + let zero = S.(may_saturate zero) - let min = Saturation_repr.min + let min = S.min - let max = Saturation_repr.max + let max = S.max - let compare = Saturation_repr.compare + let compare = S.compare - let ( < ) = Saturation_repr.( < ) + let ( < ) = S.( < ) - let ( <> ) = Saturation_repr.( <> ) + let ( <> ) = S.( <> ) - let ( > ) = Saturation_repr.( > ) + let ( > ) = S.( > ) - let ( <= ) = Saturation_repr.( <= ) + let ( <= ) = S.( <= ) - let ( >= ) = Saturation_repr.( >= ) + let ( >= ) = S.( >= ) - let ( = ) = Saturation_repr.( = ) + let ( = ) = S.( = ) - let equal = Saturation_repr.equal + let equal = S.equal - let of_int_opt = Saturation_repr.of_int_opt + let of_int_opt = S.of_int_opt let fatally_saturated_int i = failwith (string_of_int i ^ " should not be saturated.") @@ -83,7 +85,7 @@ module Arith = struct failwith (Z.to_string z ^ " should not be saturated.") let integral_of_int_exn i = - Saturation_repr.( + S.( match of_int_opt i with | None -> fatally_saturated_int i @@ -98,28 +100,27 @@ module Arith = struct | exception Z.Overflow -> fatally_saturated_z z - let integral_to_z (i : integral) : Z.t = - Saturation_repr.(to_z (ediv i scaling_factor)) + let integral_to_z (i : integral) : Z.t = S.(to_z (ediv i scaling_factor)) let ceil x = - let r = Saturation_repr.erem x scaling_factor in + let r = S.erem x scaling_factor in if r = zero then x else add x (sub scaling_factor r) - let floor x = sub x (Saturation_repr.erem x scaling_factor) + let floor x = sub x (S.erem x scaling_factor) let fp x = x let pp fmtr fp = - let q = Saturation_repr.(ediv fp scaling_factor |> to_int) in - let r = Saturation_repr.(erem fp scaling_factor |> to_int) in + let q = S.(ediv fp scaling_factor |> to_int) in + let r = S.(erem fp scaling_factor |> to_int) in if Compare.Int.(r = 0) then Format.fprintf fmtr "%d" q else Format.fprintf fmtr "%d.%0*d" q decimals r let pp_integral = pp - let n_fp_encoding : fp Data_encoding.t = Saturation_repr.n_encoding + let n_fp_encoding : fp Data_encoding.t = S.n_encoding - let z_fp_encoding : fp Data_encoding.t = Saturation_repr.z_encoding + let z_fp_encoding : fp Data_encoding.t = S.z_encoding let n_integral_encoding : integral Data_encoding.t = Data_encoding.conv integral_to_z integral_exn Data_encoding.n @@ -134,13 +135,11 @@ module Arith = struct | None -> fatally_saturated_z x - let sub_opt = Saturation_repr.sub_opt + let sub_opt = S.sub_opt end type t = Unaccounted | Limited of {remaining : Arith.fp} -module S = Saturation_repr - type cost = S.may_saturate S.t let encoding = @@ -206,12 +205,10 @@ let step_cost n = S.mul step_weight n let free = S.zero |> S.may_saturate let read_bytes_cost n = - S.add read_base_weight (S.mul byte_read_weight (Saturation_repr.safe_int n)) + S.add read_base_weight (S.mul byte_read_weight (S.safe_int n)) let write_bytes_cost n = - S.add - write_base_weight - (S.mul byte_written_weight (Saturation_repr.safe_int n)) + S.add write_base_weight (S.mul byte_written_weight (S.safe_int n)) let ( +@ ) x y = S.add x y -- GitLab From 947d904e6f3c8f6942d4478a6d6002f3e2499cce Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Wed, 27 Jan 2021 10:01:56 +0100 Subject: [PATCH 08/23] Proto: Give an explicit definition for mul_safe integers Signed-off-by: Yann Regis-Gianas --- src/proto_alpha/lib_protocol/saturation_repr.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/proto_alpha/lib_protocol/saturation_repr.mli b/src/proto_alpha/lib_protocol/saturation_repr.mli index 1618e2e31dfc..3387c63ff826 100644 --- a/src/proto_alpha/lib_protocol/saturation_repr.mli +++ b/src/proto_alpha/lib_protocol/saturation_repr.mli @@ -106,7 +106,8 @@ val shift_right : 'a t -> int -> 'a t val mul : _ t -> _ t -> may_saturate t (** [mul_safe x] returns a [mul_safe t] only if [x] does not trigger - overflows when multiplied with another [mul_safe t]. *) + overflows when multiplied with another [mul_safe t]. More precisely, + [x] is safe for fast multiplications if [x < 2147483648]. *) val mul_safe : _ t -> mul_safe t option (** [mul_fast x y] exploits the fact that [x] and [y] are known not to -- GitLab From f3eafde0cf329302902d0fcbb93e09f850637151 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Wed, 27 Jan 2021 10:02:23 +0100 Subject: [PATCH 09/23] Proto: Optimize some multiplications in the cost model Signed-off-by: Yann Regis-Gianas --- .../lib_protocol/gas_limit_repr.ml | 59 ++++++++++++------- 1 file changed, 39 insertions(+), 20 deletions(-) diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.ml b/src/proto_alpha/lib_protocol/gas_limit_repr.ml index 460367eb4368..85026276c48e 100644 --- a/src/proto_alpha/lib_protocol/gas_limit_repr.ml +++ b/src/proto_alpha/lib_protocol/gas_limit_repr.ml @@ -31,13 +31,35 @@ type integral_tag module S = Saturation_repr +(* + + When a saturated integer is sufficiently small (i.e. strictly less + than 2147483648), we can assign it the type [mul_safe S.t] to use + it within fast multiplications, named [S.scale_fast] and + [S.mul_fast]. + + The following function allows such type assignment but may raise an + exception if the assumption is wrong. Therefore, [assert_mul_safe] + should only be used to define toplevel values, so that these + exceptions can only occur during startup. + +*) +let assert_mul_safe x = + match S.mul_safe x with None -> assert false | Some x -> x + +(* + + Similarly as [assert_mul_safe], [safe_const] must only be applied + to integer literals that are small enough for fast multiplications. + +*) let safe_const x = - match S.(Option.bind (of_int_opt x) mul_safe) with + match S.of_int_opt x with | None -> - (* because [safe_const] is always called with small enough constants. *) + (* Since [safe_const] is only applied to small integers: *) assert false | Some x -> - x + assert_mul_safe x let scaling_factor = safe_const 1000 @@ -168,17 +190,22 @@ let cost_encoding = S.z_encoding let pp_cost fmt z = S.pp fmt z -let allocation_weight = S.(mul_fast scaling_factor (safe_const 2)) +let allocation_weight = + S.(mul_fast scaling_factor (safe_const 2)) |> assert_mul_safe let step_weight = scaling_factor -let read_base_weight = S.(mul_fast scaling_factor (safe_const 100)) +let read_base_weight = + S.(mul_fast scaling_factor (safe_const 100)) |> assert_mul_safe -let write_base_weight = S.(mul_fast scaling_factor (safe_const 160)) +let write_base_weight = + S.(mul_fast scaling_factor (safe_const 160)) |> assert_mul_safe -let byte_read_weight = S.(mul_fast scaling_factor (safe_const 10)) +let byte_read_weight = + S.(mul_fast scaling_factor (safe_const 10)) |> assert_mul_safe -let byte_written_weight = S.(mul_fast scaling_factor (safe_const 15)) +let byte_written_weight = + S.(mul_fast scaling_factor (safe_const 15)) |> assert_mul_safe let cost_to_milligas (cost : cost) : Arith.fp = cost @@ -186,17 +213,9 @@ let raw_consume gas_counter cost = let gas = cost_to_milligas cost in Arith.sub_opt gas_counter gas -let alloc_cost n = S.mul allocation_weight S.(add n (safe_const 1)) +let alloc_cost n = S.scale_fast allocation_weight S.(add n (safe_const 1)) -let alloc_bytes_cost n = - match S.of_int_opt ((n + 7) / 8) with - | None -> - (* Since [n] is supposed to be positive, the following case should - never occur. In case this assumption does not hold, we return - [saturated], which is always a safe cost. *) - S.saturated - | Some x -> - alloc_cost x +let alloc_bytes_cost n = S.safe_int ((n + 7) / 8) let atomic_step_cost : 'a S.t -> cost = S.may_saturate @@ -205,10 +224,10 @@ let step_cost n = S.mul step_weight n let free = S.zero |> S.may_saturate let read_bytes_cost n = - S.add read_base_weight (S.mul byte_read_weight (S.safe_int n)) + S.add read_base_weight (S.scale_fast byte_read_weight (S.safe_int n)) let write_bytes_cost n = - S.add write_base_weight (S.mul byte_written_weight (S.safe_int n)) + S.add write_base_weight (S.scale_fast byte_written_weight (S.safe_int n)) let ( +@ ) x y = S.add x y -- GitLab From a1dc88d25472e266285f1c104222eaf686f6409b Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Wed, 27 Jan 2021 10:09:29 +0100 Subject: [PATCH 10/23] Proto: Simplify the gas model implementation Signed-off-by: Yann Regis-Gianas --- .../lib_protocol/michelson_v1_gas.ml | 345 ++++++++---------- 1 file changed, 162 insertions(+), 183 deletions(-) diff --git a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml index b8a1cfebfa88..4fadef1c59f3 100644 --- a/src/proto_alpha/lib_protocol/michelson_v1_gas.ml +++ b/src/proto_alpha/lib_protocol/michelson_v1_gas.ml @@ -32,12 +32,7 @@ module S = Saturation_repr module Cost_of = struct module S_syntax = struct (* This is a good enough approximation. S.numbits 0 = 0 *) - let log2 x = - match S.of_int_opt (1 + Z.numbits (S.to_z x)) with - | None -> - S.saturated - | Some x -> - x + let log2 x = S.safe_int (1 + Z.numbits (S.to_z x)) let ( + ) = S.add @@ -50,22 +45,6 @@ module Cost_of = struct let bits = Z.numbits z in (7 + bits) / 8 - let mul_safe_const x = - match S.(Option.bind (of_int_opt x) mul_safe) with - | None -> - (* Because [mul_safe_const] is applied to small enough literals: *) - assert false - | Some x -> - x - - let safe_const x = - match S.(of_int_opt x) with - | None -> - (* Because [safe_const] is applied to small literals: *) - assert false - | Some x -> - x - let int_bytes (z : 'a Script_int.num) = z_bytes (Script_int.to_zint z) let timestamp_bytes (t : Script_timestamp.t) = @@ -79,7 +58,7 @@ module Cost_of = struct fun wit v -> match (wit, v) with | (Unit_key _, _) -> - safe_const 1 + S.safe_int 1 | (Never_key _, _) -> . | (Int_key _, _) -> @@ -87,37 +66,37 @@ module Cost_of = struct | (Nat_key _, _) -> S.safe_int @@ int_bytes v | (Signature_key _, _) -> - safe_const Signature.size + S.safe_int Signature.size | (String_key _, _) -> S.safe_int @@ String.length v | (Bytes_key _, _) -> S.safe_int @@ Bytes.length v | (Bool_key _, _) -> - safe_const 8 + S.safe_int 8 | (Key_hash_key _, _) -> - safe_const Signature.Public_key_hash.size + S.safe_int Signature.Public_key_hash.size | (Key_key _, k) -> S.safe_int @@ Signature.Public_key.size k | (Timestamp_key _, _) -> S.safe_int @@ timestamp_bytes v | (Address_key _, _) -> - safe_const Signature.Public_key_hash.size + S.safe_int Signature.Public_key_hash.size | (Mutez_key _, _) -> - safe_const 8 + S.safe_int 8 | (Chain_id_key _, _) -> - safe_const Chain_id.size + S.safe_int Chain_id.size | (Pair_key ((l, _), (r, _), _), (lval, rval)) -> S.add (size_of_comparable l lval) (size_of_comparable r rval) | (Union_key ((t, _), _, _), L x) -> - S.add (safe_const 1) (size_of_comparable t x) + S.add (S.safe_int 1) (size_of_comparable t x) | (Union_key (_, (t, _), _), R x) -> - S.add (safe_const 1) (size_of_comparable t x) + S.add (S.safe_int 1) (size_of_comparable t x) | (Option_key _, None) -> - safe_const 1 + S.safe_int 1 | (Option_key (t, _), Some x) -> - S.add (safe_const 1) (size_of_comparable t x) + S.add (S.safe_int 1) (size_of_comparable t x) - let manager_operation = step_cost @@ mul_safe_const 1_000 + let manager_operation = step_cost @@ S.safe_int 1_000 (* FIXME: hardcoded constant, available in next environment version. Set to a reasonable upper bound. *) @@ -132,15 +111,15 @@ module Cost_of = struct (* model N_Add_bls12_381_fr *) - let cost_N_Add_bls12_381_fr = safe_const 230 + let cost_N_Add_bls12_381_fr = S.safe_int 230 (* model N_Add_bls12_381_g1 *) - let cost_N_Add_bls12_381_g1 = safe_const 9_300 + let cost_N_Add_bls12_381_g1 = S.safe_int 9_300 (* model N_Add_bls12_381_g2 *) - let cost_N_Add_bls12_381_g2 = safe_const 13_000 + let cost_N_Add_bls12_381_g2 = S.safe_int 13_000 (* model N_Add_intint *) (* Approximating 0.082158 x term *) @@ -149,10 +128,10 @@ module Cost_of = struct S.safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) (* model N_Add_tez *) - let cost_N_Add_tez = safe_const 100 + let cost_N_Add_tez = S.safe_int 100 (* model N_And *) - let cost_N_And = safe_const 100 + let cost_N_And = S.safe_int 100 (* model N_And_nat *) (* Approximating 0.079325 x term *) @@ -168,31 +147,31 @@ module Cost_of = struct S.safe_int 500 + (size + (size lsr 2)) (* model N_Car *) - let cost_N_Car = safe_const 80 + let cost_N_Car = S.safe_int 80 (* model N_Cdr *) - let cost_N_Cdr = safe_const 80 + let cost_N_Cdr = S.safe_int 80 (* model N_Check_signature_ed25519 *) (* Approximating 1.372685 x term *) let cost_N_Check_signature_ed25519 size = let open S_syntax in let size = S.safe_int size in - safe_const 270_000 + (size + (size lsr 2)) + S.safe_int 270_000 + (size + (size lsr 2)) (* model N_Check_signature_p256 *) (* Approximating 1.385771 x term *) let cost_N_Check_signature_p256 size = let open S_syntax in let size = S.safe_int size in - safe_const 600_000 + (size + (size lsr 2) + (size lsr 3)) + S.safe_int 600_000 + (size + (size lsr 2) + (size lsr 3)) (* model N_Check_signature_secp256k1 *) (* Approximating 1.372411 x term *) let cost_N_Check_signature_secp256k1 size = let open S_syntax in let size = S.safe_int size in - safe_const 60_000 + (size + (size lsr 2)) + S.safe_int 60_000 + (size + (size lsr 2)) (* model N_Comb *) (* Approximating 3.275337 x term *) @@ -248,31 +227,31 @@ module Cost_of = struct S.safe_int 80 + (v0 lsr 4) (* model N_Cons_list *) - let cost_N_Cons_list = safe_const 80 + let cost_N_Cons_list = S.safe_int 80 (* model N_Cons_none *) - let cost_N_Cons_none = safe_const 80 + let cost_N_Cons_none = S.safe_int 80 (* model N_Cons_pair *) - let cost_N_Cons_pair = safe_const 80 + let cost_N_Cons_pair = S.safe_int 80 (* model N_Cons_some *) - let cost_N_Cons_some = safe_const 80 + let cost_N_Cons_some = S.safe_int 80 (* model N_Const *) - let cost_N_Const = safe_const 80 + let cost_N_Const = S.safe_int 80 (* model N_Dig *) let cost_N_Dig size = S.safe_int (100 + (4 * size)) (* model N_Dip *) - let cost_N_Dip = safe_const 100 + let cost_N_Dip = S.safe_int 100 (* model N_DipN *) let cost_N_DipN size = S.safe_int (100 + (4 * size)) (* model N_Drop *) - let cost_N_Drop = safe_const 80 + let cost_N_Drop = S.safe_int 80 (* model N_DropN *) let cost_N_DropN size = S.safe_int (100 + (4 * size)) @@ -291,72 +270,72 @@ module Cost_of = struct (* Approximating 0.001599 x term *) let cost_N_Ediv_natnat size1 size2 = let q = size1 - size2 in - if Compare.Int.(q < 0) then safe_const 300 + if Compare.Int.(q < 0) then S.safe_int 300 else let open S_syntax in let v0 = S.safe_int q * S.safe_int size2 in - safe_const 300 + (v0 lsr 10) + (v0 lsr 11) + (v0 lsr 13) + S.safe_int 300 + (v0 lsr 10) + (v0 lsr 11) + (v0 lsr 13) (* model N_Ediv_tez *) - let cost_N_Ediv_tez = safe_const 200 + let cost_N_Ediv_tez = S.safe_int 200 (* model N_Ediv_teznat *) (* Extracted by hand from the empirical data *) - let cost_N_Ediv_teznat = safe_const 300 + let cost_N_Ediv_teznat = S.safe_int 300 (* model N_Empty_map *) - let cost_N_Empty_map = safe_const 240 + let cost_N_Empty_map = S.safe_int 240 (* model N_Empty_set *) - let cost_N_Empty_set = safe_const 240 + let cost_N_Empty_set = S.safe_int 240 (* model N_Eq *) - let cost_N_Eq = safe_const 80 + let cost_N_Eq = S.safe_int 80 (* model N_If *) - let cost_N_If = safe_const 60 + let cost_N_If = S.safe_int 60 (* model N_If_cons *) - let cost_N_If_cons = safe_const 110 + let cost_N_If_cons = S.safe_int 110 (* model N_If_left *) - let cost_N_If_left = safe_const 90 + let cost_N_If_left = S.safe_int 90 (* model N_If_none *) - let cost_N_If_none = safe_const 80 + let cost_N_If_none = S.safe_int 80 (* model N_Int_nat *) - let cost_N_Int_nat = safe_const 80 + let cost_N_Int_nat = S.safe_int 80 (* model N_Is_nat *) - let cost_N_Is_nat = safe_const 80 + let cost_N_Is_nat = S.safe_int 80 (* model N_Keccak *) let cost_N_Keccak size = let open S_syntax in - safe_const 1_400 + (safe_const 30 * S.safe_int size) + S.safe_int 1_400 + (S.safe_int 30 * S.safe_int size) (* model N_Left *) - let cost_N_Left = safe_const 80 + let cost_N_Left = S.safe_int 80 (* model N_List_iter *) let cost_N_List_iter size = let open S_syntax in - safe_const 500 + (safe_const 7 * S.safe_int size) + S.safe_int 500 + (S.safe_int 7 * S.safe_int size) (* model N_List_map *) let cost_N_List_map size = let open S_syntax in - safe_const 500 + (safe_const 12 * S.safe_int size) + S.safe_int 500 + (S.safe_int 12 * S.safe_int size) (* model N_List_size *) - let cost_N_List_size = safe_const 80 + let cost_N_List_size = S.safe_int 80 (* model N_Loop *) - let cost_N_Loop = safe_const 70 + let cost_N_Loop = S.safe_int 70 (* model N_Loop_left *) - let cost_N_Loop_left = safe_const 80 + let cost_N_Loop_left = S.safe_int 80 (* model N_Lsl_nat *) (* Approximating 0.129443 x term *) @@ -371,51 +350,51 @@ module Cost_of = struct let cost_N_Map_get size1 size2 = let open S_syntax in let v0 = size1 * log2 size2 in - safe_const 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) + S.safe_int 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) (* model N_Map_iter *) let cost_N_Map_iter size = let open S_syntax in - safe_const 80 + (safe_const 40 * S.safe_int size) + S.safe_int 80 + (S.safe_int 40 * S.safe_int size) (* model N_Map_map *) let cost_N_Map_map size = let open S_syntax in - safe_const 80 + (safe_const 761 * S.safe_int size) + S.safe_int 80 + (S.safe_int 761 * S.safe_int size) (* model N_Map_mem *) (* Approximating 0.058563 x term *) let cost_N_Map_mem size1 size2 = let open S_syntax in let v0 = size1 * log2 size2 in - safe_const 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) + S.safe_int 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) (* model N_Map_size *) - let cost_N_Map_size = safe_const 90 + let cost_N_Map_size = S.safe_int 90 (* model N_Map_update *) (* Approximating 0.119968 x term *) let cost_N_Map_update size1 size2 = let open S_syntax in let v0 = size1 * log2 size2 in - safe_const 80 + (v0 lsr 4) + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) + S.safe_int 80 + (v0 lsr 4) + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) (* model N_Mul_bls12_381_fr *) - let cost_N_Mul_bls12_381_fr = safe_const 260 + let cost_N_Mul_bls12_381_fr = S.safe_int 260 (* model N_Mul_bls12_381_g1 *) - let cost_N_Mul_bls12_381_g1 = safe_const 265_000 + let cost_N_Mul_bls12_381_g1 = S.safe_int 265_000 (* model N_Mul_bls12_381_g2 *) - let cost_N_Mul_bls12_381_g2 = safe_const 850_000 + let cost_N_Mul_bls12_381_g2 = S.safe_int 850_000 (* Converting fr from/to S.t *) - let cost_bls12_381_fr_of_z = safe_const 130 + let cost_bls12_381_fr_of_z = S.safe_int 130 - let cost_bls12_381_fr_to_z = safe_const 30 + let cost_bls12_381_fr_to_z = S.safe_int 30 let cost_N_Mul_bls12_381_fr_z = S.add cost_bls12_381_fr_of_z cost_N_Mul_bls12_381_fr @@ -426,47 +405,47 @@ module Cost_of = struct let cost_N_Mul_intint size1 size2 = let open S_syntax in let a = S.add (S.safe_int size1) (S.safe_int size2) in - safe_const 80 + (a * log2 a) + S.safe_int 80 + (a * log2 a) (* model N_Mul_teznat *) let cost_N_Mul_teznat size = let open S_syntax in - safe_const 200 + (safe_const 133 * S.safe_int size) + S.safe_int 200 + (S.safe_int 133 * S.safe_int size) (* model N_Neg_bls12_381_fr *) - let cost_N_Neg_bls12_381_fr = safe_const 180 + let cost_N_Neg_bls12_381_fr = S.safe_int 180 (* model N_Neg_bls12_381_g1 *) - let cost_N_Neg_bls12_381_g1 = safe_const 410 + let cost_N_Neg_bls12_381_g1 = S.safe_int 410 (* model N_Neg_bls12_381_g2 *) - let cost_N_Neg_bls12_381_g2 = safe_const 715 + let cost_N_Neg_bls12_381_g2 = S.safe_int 715 (* model N_Neg_int *) (* Approximating 0.068419 x term *) let cost_N_Neg_int size = S.safe_int (80 + (size lsr 4)) (* model N_Neq *) - let cost_N_Neq = safe_const 80 + let cost_N_Neq = S.safe_int 80 (* model N_Nil *) - let cost_N_Nil = safe_const 80 + let cost_N_Nil = S.safe_int 80 (* model N_Nop *) - let cost_N_Nop = safe_const 70 + let cost_N_Nop = S.safe_int 70 (* model N_Not *) - let cost_N_Not = safe_const 90 + let cost_N_Not = S.safe_int 90 (* model N_Not_int *) (* Approximating 0.076564 x term *) let cost_N_Not_int size = S.safe_int (55 + ((size lsr 4) + (size lsr 7))) (* model N_Or *) - let cost_N_Or = safe_const 90 + let cost_N_Or = S.safe_int 90 (* model N_Or_nat *) (* Approximating 0.078718 x term *) @@ -478,58 +457,58 @@ module Cost_of = struct let cost_N_Pairing_check_bls12_381 size = S.add - (safe_const 1_550_000) - (S.mul (safe_const 510_000) (S.safe_int size)) + (S.safe_int 1_550_000) + (S.mul (S.safe_int 510_000) (S.safe_int size)) (* model N_Right *) - let cost_N_Right = safe_const 80 + let cost_N_Right = S.safe_int 80 (* model N_Seq *) - let cost_N_Seq = safe_const 60 + let cost_N_Seq = S.safe_int 60 (* model N_Set_iter *) let cost_N_Set_iter size = let open S_syntax in - safe_const 80 + (safe_const 36 * S.safe_int size) + S.safe_int 80 + (S.safe_int 36 * S.safe_int size) (* model N_Set_mem *) (* Approximating 0.059410 x term *) let cost_N_Set_mem size1 size2 = let open S_syntax in let v0 = size1 * log2 (S.safe_int size2) in - safe_const 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) + (v0 lsr 8) + S.safe_int 80 + (v0 lsr 5) + (v0 lsr 6) + (v0 lsr 7) + (v0 lsr 8) (* model N_Set_size *) - let cost_N_Set_size = safe_const 80 + let cost_N_Set_size = S.safe_int 80 (* model N_Set_update *) (* Approximating 0.126260 x term *) let cost_N_Set_update size1 size2 = let open S_syntax in let v0 = size1 * log2 (S.safe_int size2) in - safe_const 80 + (v0 lsr 3) + S.safe_int 80 + (v0 lsr 3) (* model N_Sha256 *) let cost_N_Sha256 size = let open S_syntax in - safe_const 500 + (safe_const 5 * S.safe_int size) + S.safe_int 500 + (S.safe_int 5 * S.safe_int size) (* model N_Sha3 *) let cost_N_Sha3 size = let open S_syntax in - safe_const 1_400 + (safe_const 32 * S.safe_int size) + S.safe_int 1_400 + (S.safe_int 32 * S.safe_int size) (* model N_Sha512 *) let cost_N_Sha512 size = let open S_syntax in - safe_const 500 + (safe_const 3 * S.safe_int size) + S.safe_int 500 + (S.safe_int 3 * S.safe_int size) (* model N_Slice_string *) (* Approximating 0.067048 x term *) let cost_N_Slice_string size = S.safe_int (80 + (size lsr 4)) (* model N_String_size *) - let cost_N_String_size = safe_const 80 + let cost_N_String_size = S.safe_int 80 (* model N_Sub_int *) (* Approximating 0.082399 x term *) @@ -538,13 +517,13 @@ module Cost_of = struct S.safe_int (80 + ((v0 lsr 4) + (v0 lsr 6))) (* model N_Sub_tez *) - let cost_N_Sub_tez = safe_const 80 + let cost_N_Sub_tez = S.safe_int 80 (* model N_Swap *) - let cost_N_Swap = safe_const 70 + let cost_N_Swap = S.safe_int 70 (* model N_Total_voting_power *) - let cost_N_Total_voting_power = safe_const 400 + let cost_N_Total_voting_power = S.safe_int 400 (* model N_Uncomb *) (* Approximating 3.666332 x term *) @@ -552,13 +531,13 @@ module Cost_of = struct S.safe_int (80 + ((3 * size) + (size lsr 1) + (size lsr 3))) (* model N_Unpair *) - let cost_N_Unpair = safe_const 80 + let cost_N_Unpair = S.safe_int 80 (* model N_Voting_power *) - let cost_N_Voting_power = safe_const 400 + let cost_N_Voting_power = S.safe_int 400 (* model N_Xor *) - let cost_N_Xor = safe_const 100 + let cost_N_Xor = S.safe_int 100 (* model N_Xor_nat *) (* Approximating 0.078258 x term *) @@ -568,198 +547,198 @@ module Cost_of = struct (* model DECODING_BLS_FR *) - let cost_DECODING_BLS_FR = mul_safe_const 50 + let cost_DECODING_BLS_FR = S.safe_int 50 (* model DECODING_BLS_G1 *) - let cost_DECODING_BLS_G1 = mul_safe_const 230_000 + let cost_DECODING_BLS_G1 = S.safe_int 230_000 (* model DECODING_BLS_G2 *) - let cost_DECODING_BLS_G2 = safe_const 740_000 + let cost_DECODING_BLS_G2 = S.safe_int 740_000 (* model B58CHECK_DECODING_CHAIN_ID *) - let cost_B58CHECK_DECODING_CHAIN_ID = safe_const 1_500 + let cost_B58CHECK_DECODING_CHAIN_ID = S.safe_int 1_500 (* model B58CHECK_DECODING_PUBLIC_KEY_HASH_ed25519 *) - let cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_ed25519 = safe_const 3_300 + let cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_ed25519 = S.safe_int 3_300 (* model B58CHECK_DECODING_PUBLIC_KEY_HASH_p256 *) - let cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_p256 = safe_const 3_300 + let cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_p256 = S.safe_int 3_300 (* model B58CHECK_DECODING_PUBLIC_KEY_HASH_secp256k1 *) - let cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_secp256k1 = safe_const 3_300 + let cost_B58CHECK_DECODING_PUBLIC_KEY_HASH_secp256k1 = S.safe_int 3_300 (* model B58CHECK_DECODING_PUBLIC_KEY_ed25519 *) - let cost_B58CHECK_DECODING_PUBLIC_KEY_ed25519 = safe_const 4_300 + let cost_B58CHECK_DECODING_PUBLIC_KEY_ed25519 = S.safe_int 4_300 (* model B58CHECK_DECODING_PUBLIC_KEY_p256 *) - let cost_B58CHECK_DECODING_PUBLIC_KEY_p256 = safe_const 29_000 + let cost_B58CHECK_DECODING_PUBLIC_KEY_p256 = S.safe_int 29_000 (* model B58CHECK_DECODING_PUBLIC_KEY_secp256k1 *) - let cost_B58CHECK_DECODING_PUBLIC_KEY_secp256k1 = safe_const 9_400 + let cost_B58CHECK_DECODING_PUBLIC_KEY_secp256k1 = S.safe_int 9_400 (* model B58CHECK_DECODING_SIGNATURE_ed25519 *) - let cost_B58CHECK_DECODING_SIGNATURE_ed25519 = safe_const 6_600 + let cost_B58CHECK_DECODING_SIGNATURE_ed25519 = S.safe_int 6_600 (* model B58CHECK_DECODING_SIGNATURE_p256 *) - let cost_B58CHECK_DECODING_SIGNATURE_p256 = safe_const 6_600 + let cost_B58CHECK_DECODING_SIGNATURE_p256 = S.safe_int 6_600 (* model B58CHECK_DECODING_SIGNATURE_secp256k1 *) - let cost_B58CHECK_DECODING_SIGNATURE_secp256k1 = safe_const 6_600 + let cost_B58CHECK_DECODING_SIGNATURE_secp256k1 = S.safe_int 6_600 (* model ENCODING_BLS_FR *) - let cost_ENCODING_BLS_FR = safe_const 30 + let cost_ENCODING_BLS_FR = S.safe_int 30 (* model ENCODING_BLS_G1 *) - let cost_ENCODING_BLS_G1 = safe_const 30 + let cost_ENCODING_BLS_G1 = S.safe_int 30 (* model ENCODING_BLS_G2 *) - let cost_ENCODING_BLS_G2 = safe_const 30 + let cost_ENCODING_BLS_G2 = S.safe_int 30 (* model B58CHECK_ENCODING_CHAIN_ID *) - let cost_B58CHECK_ENCODING_CHAIN_ID = safe_const 1_600 + let cost_B58CHECK_ENCODING_CHAIN_ID = S.safe_int 1_600 (* model B58CHECK_ENCODING_PUBLIC_KEY_HASH_ed25519 *) - let cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_ed25519 = safe_const 3_300 + let cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_ed25519 = S.safe_int 3_300 (* model B58CHECK_ENCODING_PUBLIC_KEY_HASH_p256 *) - let cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_p256 = safe_const 3_750 + let cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_p256 = S.safe_int 3_750 (* model B58CHECK_ENCODING_PUBLIC_KEY_HASH_secp256k1 *) - let cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_secp256k1 = safe_const 3_300 + let cost_B58CHECK_ENCODING_PUBLIC_KEY_HASH_secp256k1 = S.safe_int 3_300 (* model B58CHECK_ENCODING_PUBLIC_KEY_ed25519 *) - let cost_B58CHECK_ENCODING_PUBLIC_KEY_ed25519 = safe_const 4_500 + let cost_B58CHECK_ENCODING_PUBLIC_KEY_ed25519 = S.safe_int 4_500 (* model B58CHECK_ENCODING_PUBLIC_KEY_p256 *) - let cost_B58CHECK_ENCODING_PUBLIC_KEY_p256 = safe_const 5_300 + let cost_B58CHECK_ENCODING_PUBLIC_KEY_p256 = S.safe_int 5_300 (* model B58CHECK_ENCODING_PUBLIC_KEY_secp256k1 *) - let cost_B58CHECK_ENCODING_PUBLIC_KEY_secp256k1 = safe_const 5_000 + let cost_B58CHECK_ENCODING_PUBLIC_KEY_secp256k1 = S.safe_int 5_000 (* model B58CHECK_ENCODING_SIGNATURE_ed25519 *) - let cost_B58CHECK_ENCODING_SIGNATURE_ed25519 = safe_const 8_700 + let cost_B58CHECK_ENCODING_SIGNATURE_ed25519 = S.safe_int 8_700 (* model B58CHECK_ENCODING_SIGNATURE_p256 *) - let cost_B58CHECK_ENCODING_SIGNATURE_p256 = safe_const 8_700 + let cost_B58CHECK_ENCODING_SIGNATURE_p256 = S.safe_int 8_700 (* model B58CHECK_ENCODING_SIGNATURE_secp256k1 *) - let cost_B58CHECK_ENCODING_SIGNATURE_secp256k1 = safe_const 8_700 + let cost_B58CHECK_ENCODING_SIGNATURE_secp256k1 = S.safe_int 8_700 (* model DECODING_CHAIN_ID *) - let cost_DECODING_CHAIN_ID = safe_const 50 + let cost_DECODING_CHAIN_ID = S.safe_int 50 (* model DECODING_PUBLIC_KEY_HASH_ed25519 *) - let cost_DECODING_PUBLIC_KEY_HASH_ed25519 = safe_const 50 + let cost_DECODING_PUBLIC_KEY_HASH_ed25519 = S.safe_int 50 (* model DECODING_PUBLIC_KEY_HASH_p256 *) - let cost_DECODING_PUBLIC_KEY_HASH_p256 = safe_const 60 + let cost_DECODING_PUBLIC_KEY_HASH_p256 = S.safe_int 60 (* model DECODING_PUBLIC_KEY_HASH_secp256k1 *) - let cost_DECODING_PUBLIC_KEY_HASH_secp256k1 = safe_const 60 + let cost_DECODING_PUBLIC_KEY_HASH_secp256k1 = S.safe_int 60 (* model DECODING_PUBLIC_KEY_ed25519 *) - let cost_DECODING_PUBLIC_KEY_ed25519 = safe_const 60 + let cost_DECODING_PUBLIC_KEY_ed25519 = S.safe_int 60 (* model DECODING_PUBLIC_KEY_p256 *) - let cost_DECODING_PUBLIC_KEY_p256 = safe_const 25_000 + let cost_DECODING_PUBLIC_KEY_p256 = S.safe_int 25_000 (* model DECODING_PUBLIC_KEY_secp256k1 *) - let cost_DECODING_PUBLIC_KEY_secp256k1 = safe_const 5_300 + let cost_DECODING_PUBLIC_KEY_secp256k1 = S.safe_int 5_300 (* model DECODING_SIGNATURE_ed25519 *) - let cost_DECODING_SIGNATURE_ed25519 = safe_const 30 + let cost_DECODING_SIGNATURE_ed25519 = S.safe_int 30 (* model DECODING_SIGNATURE_p256 *) - let cost_DECODING_SIGNATURE_p256 = safe_const 30 + let cost_DECODING_SIGNATURE_p256 = S.safe_int 30 (* model DECODING_SIGNATURE_secp256k1 *) - let cost_DECODING_SIGNATURE_secp256k1 = safe_const 30 + let cost_DECODING_SIGNATURE_secp256k1 = S.safe_int 30 (* model ENCODING_CHAIN_ID *) - let cost_ENCODING_CHAIN_ID = safe_const 50 + let cost_ENCODING_CHAIN_ID = S.safe_int 50 (* model ENCODING_PUBLIC_KEY_HASH_ed25519 *) - let cost_ENCODING_PUBLIC_KEY_HASH_ed25519 = safe_const 70 + let cost_ENCODING_PUBLIC_KEY_HASH_ed25519 = S.safe_int 70 (* model ENCODING_PUBLIC_KEY_HASH_p256 *) - let cost_ENCODING_PUBLIC_KEY_HASH_p256 = safe_const 80 + let cost_ENCODING_PUBLIC_KEY_HASH_p256 = S.safe_int 80 (* model ENCODING_PUBLIC_KEY_HASH_secp256k1 *) - let cost_ENCODING_PUBLIC_KEY_HASH_secp256k1 = safe_const 70 + let cost_ENCODING_PUBLIC_KEY_HASH_secp256k1 = S.safe_int 70 (* model ENCODING_PUBLIC_KEY_ed25519 *) - let cost_ENCODING_PUBLIC_KEY_ed25519 = safe_const 80 + let cost_ENCODING_PUBLIC_KEY_ed25519 = S.safe_int 80 (* model ENCODING_PUBLIC_KEY_p256 *) - let cost_ENCODING_PUBLIC_KEY_p256 = safe_const 450 + let cost_ENCODING_PUBLIC_KEY_p256 = S.safe_int 450 (* model ENCODING_PUBLIC_KEY_secp256k1 *) - let cost_ENCODING_PUBLIC_KEY_secp256k1 = safe_const 490 + let cost_ENCODING_PUBLIC_KEY_secp256k1 = S.safe_int 490 (* model ENCODING_SIGNATURE_ed25519 *) - let cost_ENCODING_SIGNATURE_ed25519 = safe_const 40 + let cost_ENCODING_SIGNATURE_ed25519 = S.safe_int 40 (* model ENCODING_SIGNATURE_p256 *) - let cost_ENCODING_SIGNATURE_p256 = safe_const 40 + let cost_ENCODING_SIGNATURE_p256 = S.safe_int 40 (* model ENCODING_SIGNATURE_secp256k1 *) - let cost_ENCODING_SIGNATURE_secp256k1 = safe_const 40 + let cost_ENCODING_SIGNATURE_secp256k1 = S.safe_int 40 (* model TIMESTAMP_READABLE_DECODING *) - let cost_TIMESTAMP_READABLE_DECODING = safe_const 130 + let cost_TIMESTAMP_READABLE_DECODING = S.safe_int 130 (* model TIMESTAMP_READABLE_ENCODING *) - let cost_TIMESTAMP_READABLE_ENCODING = safe_const 900 + let cost_TIMESTAMP_READABLE_ENCODING = S.safe_int 900 (* model CHECK_PRINTABLE *) let cost_CHECK_PRINTABLE size = let open S_syntax in - safe_const 14 + (safe_const 10 * S.safe_int size) + S.safe_int 14 + (S.safe_int 10 * S.safe_int size) (* model MERGE_TYPES This is the estimated cost of one iteration of merge_types, extracted and copied manually from the parameter fit for the MERGE_TYPES benchmark (the model is parametric on the size of the type, which we don't have access to in O(1)). *) - let cost_MERGE_TYPES = safe_const 130 + let cost_MERGE_TYPES = S.safe_int 130 (* model TYPECHECKING_CODE This is the cost of one iteration of parse_instr, extracted by hand from the parameter fit for the TYPECHECKING_CODE benchmark. *) - let cost_TYPECHECKING_CODE = safe_const 375 + let cost_TYPECHECKING_CODE = S.safe_int 375 (* model UNPARSING_CODE This is the cost of one iteration of unparse_instr, extracted by hand from the parameter fit for the UNPARSING_CODE benchmark. *) - let cost_UNPARSING_CODE = safe_const 200 + let cost_UNPARSING_CODE = S.safe_int 200 (* model TYPECHECKING_DATA This is the cost of one iteration of parse_data, extracted by hand from the parameter fit for the TYPECHECKING_DATA benchmark. *) - let cost_TYPECHECKING_DATA = safe_const 240 + let cost_TYPECHECKING_DATA = S.safe_int 240 (* model UNPARSING_DATA This is the cost of one iteration of unparse_data, extracted by hand from the parameter fit for the UNPARSING_DATA benchmark. *) - let cost_UNPARSING_DATA = safe_const 140 + let cost_UNPARSING_DATA = S.safe_int 140 (* model PARSE_TYPE This is the cost of one iteration of parse_ty, extracted by hand from the parameter fit for the PARSE_TYPE benchmark. *) - let cost_PARSE_TYPE = safe_const 170 + let cost_PARSE_TYPE = S.safe_int 170 (* model UNPARSE_TYPE This is the cost of one iteration of unparse_ty, extracted by hand from the parameter fit for the UNPARSE_TYPE benchmark. *) - let cost_UNPARSE_TYPE = safe_const 185 + let cost_UNPARSE_TYPE = S.safe_int 185 (* TODO: benchmark *) - let cost_COMPARABLE_TY_OF_TY = safe_const 120 + let cost_COMPARABLE_TY_OF_TY = S.safe_int 120 end module Interpreter = struct @@ -1033,7 +1012,7 @@ module Cost_of = struct let sapling_verify_update ~inputs ~outputs = let open S_syntax in atomic_step_cost - ( safe_const 85_000 + ( S.safe_int 85_000 + (S.safe_int inputs * S.safe_int 4) + (S.safe_int outputs * S.safe_int 30) ) @@ -1041,13 +1020,13 @@ module Cost_of = struct (* Semi-hand-crafted models *) let compare_unit = atomic_step_cost (S.safe_int 10) - let compare_union_tag = atomic_step_cost (safe_const 10) + let compare_union_tag = atomic_step_cost (S.safe_int 10) - let compare_option_tag = atomic_step_cost (safe_const 10) + let compare_option_tag = atomic_step_cost (S.safe_int 10) let compare_bool = atomic_step_cost (cost_N_Compare_bool 1 1) - let compare_signature = atomic_step_cost (safe_const 92) + let compare_signature = atomic_step_cost (S.safe_int 92) let compare_string s1 s2 = atomic_step_cost @@ -1069,7 +1048,7 @@ module Cost_of = struct let sz = Signature.Public_key_hash.size in atomic_step_cost (cost_N_Compare_key_hash sz sz) - let compare_key = atomic_step_cost (safe_const 92) + let compare_key = atomic_step_cost (S.safe_int 92) let compare_timestamp t1 t2 = atomic_step_cost @@ -1081,7 +1060,7 @@ module Cost_of = struct let sz = Signature.Public_key_hash.size + Chain_id.size in atomic_step_cost (cost_N_Compare_address sz sz) - let compare_chain_id = atomic_step_cost (safe_const 30) + let compare_chain_id = atomic_step_cost (S.safe_int 30) let rec compare : type a. a Script_typed_ir.comparable_ty -> a -> a -> cost = @@ -1161,7 +1140,7 @@ module Cost_of = struct *) let concat_string_precheck (l : 'a Script_typed_ir.boxed_list) = (* we set the precheck to be slightly more expensive than cost_N_List_iter *) - atomic_step_cost (S.mul (S.safe_int l.length) (safe_const 10)) + atomic_step_cost (S.mul (S.safe_int l.length) (S.safe_int 10)) (* This is the cost of allocating a string and blitting existing ones into it. *) let concat_string total_bytes = @@ -1174,12 +1153,12 @@ module Cost_of = struct S.(add (S.safe_int 100) (S.ediv total_bytes (S.safe_int 10))) (* Cost of additional call to logger + overhead of setting up call to [interp]. *) - let exec = atomic_step_cost (safe_const 100) + let exec = atomic_step_cost (S.safe_int 100) (* Heavy computation happens in the [unparse_data], [unparse_ty] functions which are carbonated. We must account for allocating the Micheline lambda wrapper. *) - let apply = atomic_step_cost (safe_const 1000) + let apply = atomic_step_cost (S.safe_int 1000) (* Pushing a pointer on the stack. *) let lambda = push @@ -1211,7 +1190,7 @@ module Cost_of = struct let balance = Gas.free (* Accessing the raw_context, Small arithmetic & pushing on the stack. *) - let level = atomic_step_cost (S.mul (safe_const 2) cost_N_Const) + let level = atomic_step_cost (S.mul (S.safe_int 2) cost_N_Const) (* Same as [cost_level] *) let now = level @@ -1248,11 +1227,11 @@ module Cost_of = struct (len *@ alloc_mbytes_cost 1) +@ len *@ ( S.safe_int d - *@ (alloc_cost (safe_const 3) +@ step_cost (safe_const 1)) ) + *@ (alloc_cost (S.safe_int 3) +@ step_cost (S.safe_int 1)) ) - let ticket = atomic_step_cost (safe_const 80) + let ticket = atomic_step_cost (S.safe_int 80) - let read_ticket = atomic_step_cost (safe_const 80) + let read_ticket = atomic_step_cost (S.safe_int 80) let split_ticket ticket_amount amount_a amount_b = ticket @@ -1370,7 +1349,7 @@ module Cost_of = struct let timestamp_readable = atomic_step_cost cost_TIMESTAMP_READABLE_DECODING (* Reasonable estimate. *) - let contract = Gas.(safe_const 2 *@ public_key_readable) + let contract = Gas.(S.safe_int 2 *@ public_key_readable) (* Assuming unflattened storage: /contracts/hash1/.../hash6/key/balance, balance stored on 64 bits *) @@ -1381,7 +1360,7 @@ module Cost_of = struct (* Constructing proof arguments consists in a decreasing loop in the result monad, allocating at each step. We charge a reasonable overapproximation. *) let proof_argument n = - atomic_step_cost (S.mul (S.safe_int n) (safe_const 50)) + atomic_step_cost (S.mul (S.safe_int n) (S.safe_int 50)) end module Unparsing = struct @@ -1471,7 +1450,7 @@ module Cost_of = struct let unit = Gas.free (* Reasonable estimate. *) - let contract = Gas.(safe_const 2 *@ public_key_readable) + let contract = Gas.(S.safe_int 2 *@ public_key_readable) (* Reuse 006 costs. *) let operation bytes = Script.bytes_node_cost bytes -- GitLab From 3021da513451467ab3f5325490c36fb5d98f9278 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Wed, 27 Jan 2021 18:21:15 +0100 Subject: [PATCH 11/23] Proto: Ensure that exception-raising fun identifiers end with _exn Signed-off-by: Yann Regis-Gianas --- .../lib_protocol/gas_limit_repr.ml | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.ml b/src/proto_alpha/lib_protocol/gas_limit_repr.ml index 85026276c48e..7ef48dc4065b 100644 --- a/src/proto_alpha/lib_protocol/gas_limit_repr.ml +++ b/src/proto_alpha/lib_protocol/gas_limit_repr.ml @@ -44,24 +44,24 @@ module S = Saturation_repr exceptions can only occur during startup. *) -let assert_mul_safe x = +let assert_mul_safe_exn x = match S.mul_safe x with None -> assert false | Some x -> x (* - Similarly as [assert_mul_safe], [safe_const] must only be applied + Similarly as [assert_mul_safe_exn], [safe_const_exn] must only be applied to integer literals that are small enough for fast multiplications. *) -let safe_const x = +let safe_const_exn x = match S.of_int_opt x with | None -> - (* Since [safe_const] is only applied to small integers: *) + (* Since [safe_const_exn] is only applied to small integers: *) assert false | Some x -> - assert_mul_safe x + assert_mul_safe_exn x -let scaling_factor = safe_const 1000 +let scaling_factor = safe_const_exn 1000 module Arith = struct type 'a t = S.may_saturate S.t @@ -191,21 +191,21 @@ let cost_encoding = S.z_encoding let pp_cost fmt z = S.pp fmt z let allocation_weight = - S.(mul_fast scaling_factor (safe_const 2)) |> assert_mul_safe + S.(mul_fast scaling_factor (safe_const_exn 2)) |> assert_mul_safe_exn let step_weight = scaling_factor let read_base_weight = - S.(mul_fast scaling_factor (safe_const 100)) |> assert_mul_safe + S.(mul_fast scaling_factor (safe_const_exn 100)) |> assert_mul_safe_exn let write_base_weight = - S.(mul_fast scaling_factor (safe_const 160)) |> assert_mul_safe + S.(mul_fast scaling_factor (safe_const_exn 160)) |> assert_mul_safe_exn let byte_read_weight = - S.(mul_fast scaling_factor (safe_const 10)) |> assert_mul_safe + S.(mul_fast scaling_factor (safe_const_exn 10)) |> assert_mul_safe_exn let byte_written_weight = - S.(mul_fast scaling_factor (safe_const 15)) |> assert_mul_safe + S.(mul_fast scaling_factor (safe_const_exn 15)) |> assert_mul_safe_exn let cost_to_milligas (cost : cost) : Arith.fp = cost @@ -213,7 +213,7 @@ let raw_consume gas_counter cost = let gas = cost_to_milligas cost in Arith.sub_opt gas_counter gas -let alloc_cost n = S.scale_fast allocation_weight S.(add n (safe_const 1)) +let alloc_cost n = S.scale_fast allocation_weight S.(add n (safe_const_exn 1)) let alloc_bytes_cost n = S.safe_int ((n + 7) / 8) @@ -233,4 +233,4 @@ let ( +@ ) x y = S.add x y let ( *@ ) x y = S.mul x y -let alloc_mbytes_cost n = alloc_cost (safe_const 12) +@ alloc_bytes_cost n +let alloc_mbytes_cost n = alloc_cost (safe_const_exn 12) +@ alloc_bytes_cost n -- GitLab From c706bdd2cb9f375284212b373eb99007f2e7ba76 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Wed, 27 Jan 2021 18:24:51 +0100 Subject: [PATCH 12/23] Proto: Optimize [step_cost] Signed-off-by: Yann Regis-Gianas --- src/proto_alpha/lib_protocol/gas_limit_repr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.ml b/src/proto_alpha/lib_protocol/gas_limit_repr.ml index 7ef48dc4065b..f7d1cd9f8076 100644 --- a/src/proto_alpha/lib_protocol/gas_limit_repr.ml +++ b/src/proto_alpha/lib_protocol/gas_limit_repr.ml @@ -219,7 +219,7 @@ let alloc_bytes_cost n = S.safe_int ((n + 7) / 8) let atomic_step_cost : 'a S.t -> cost = S.may_saturate -let step_cost n = S.mul step_weight n +let step_cost n = S.scale_fast step_weight n let free = S.zero |> S.may_saturate -- GitLab From a4dfc7cf76711aac2ba3cd4409e161716d5f1b93 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Wed, 27 Jan 2021 18:28:48 +0100 Subject: [PATCH 13/23] Proto: Generalize the type of Saturation_repr.zero Signed-off-by: Yann Regis-Gianas --- src/proto_alpha/lib_protocol/gas_limit_repr.ml | 2 +- src/proto_alpha/lib_protocol/saturation_repr.mli | 2 +- src/proto_alpha/lib_protocol/script_interpreter.ml | 4 ++-- src/proto_alpha/lib_protocol/script_repr.ml | 3 +-- 4 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.ml b/src/proto_alpha/lib_protocol/gas_limit_repr.ml index f7d1cd9f8076..ded529d448d1 100644 --- a/src/proto_alpha/lib_protocol/gas_limit_repr.ml +++ b/src/proto_alpha/lib_protocol/gas_limit_repr.ml @@ -221,7 +221,7 @@ let atomic_step_cost : 'a S.t -> cost = S.may_saturate let step_cost n = S.scale_fast step_weight n -let free = S.zero |> S.may_saturate +let free = S.zero let read_bytes_cost n = S.add read_base_weight (S.scale_fast byte_read_weight (S.safe_int n)) diff --git a/src/proto_alpha/lib_protocol/saturation_repr.mli b/src/proto_alpha/lib_protocol/saturation_repr.mli index 3387c63ff826..53101f12ecaa 100644 --- a/src/proto_alpha/lib_protocol/saturation_repr.mli +++ b/src/proto_alpha/lib_protocol/saturation_repr.mli @@ -70,7 +70,7 @@ val may_saturate : _ t -> may_saturate t val to_int : 'a t -> int (** 0 *) -val zero : mul_safe t +val zero : _ t (** 2^62 - 1 *) val saturated : may_saturate t diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index 6f0966a21513..e3cf135e2543 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -779,7 +779,7 @@ let rec step_bounded : (fun acc s -> let len = S.of_int_opt (String.length s) |> S.saturate_if_undef in S.add acc len) - (S.zero |> S.may_saturate) + S.zero ss.elements in Gas.consume ctxt (Interp_costs.concat_string total_length) @@ -808,7 +808,7 @@ let rec step_bounded : (fun acc s -> let len = S.of_int_opt (Bytes.length s) |> S.saturate_if_undef in S.add acc len) - (S.zero |> S.may_saturate) + S.zero ss.elements in Gas.consume ctxt (Interp_costs.concat_string total_length) diff --git a/src/proto_alpha/lib_protocol/script_repr.ml b/src/proto_alpha/lib_protocol/script_repr.ml index dd3b4d48ac9d..b271d116b8ec 100644 --- a/src/proto_alpha/lib_protocol/script_repr.ml +++ b/src/proto_alpha/lib_protocol/script_repr.ml @@ -134,8 +134,7 @@ let traversal_cost node = let cost_of_size (blocks, words) = let open Gas_limit_repr in - S.max (S.zero |> S.may_saturate) (S.sub blocks (S.safe_int 1)) - *@ alloc_cost S.zero + (S.max S.zero (S.sub blocks (S.safe_int 1)) *@ alloc_cost S.zero) +@ alloc_cost words +@ step_cost blocks let cost_of_size_int pair = cost_of_size (convert_pair pair) -- GitLab From 4cd09cf21bbf02b928f67e5a0e2c7d2a6a24d345 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Wed, 27 Jan 2021 18:31:53 +0100 Subject: [PATCH 14/23] Proto: Avoid opening Saturation_repr only for a single type ref Signed-off-by: Yann Regis-Gianas --- src/proto_alpha/lib_protocol/gas_limit_repr.mli | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.mli b/src/proto_alpha/lib_protocol/gas_limit_repr.mli index d42591fc8668..629679f49bbc 100644 --- a/src/proto_alpha/lib_protocol/gas_limit_repr.mli +++ b/src/proto_alpha/lib_protocol/gas_limit_repr.mli @@ -23,8 +23,6 @@ (* *) (*****************************************************************************) -open Saturation_repr - module Arith : Fixed_point_repr.Full type t = Unaccounted | Limited of {remaining : Arith.fp} @@ -33,7 +31,7 @@ val encoding : t Data_encoding.encoding val pp : Format.formatter -> t -> unit -type cost = may_saturate Saturation_repr.t +type cost = Saturation_repr.may_saturate Saturation_repr.t val cost_encoding : cost Data_encoding.encoding -- GitLab From 4fa9891ec6cf9950f2a93056e7be766e05870011 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Wed, 27 Jan 2021 18:47:07 +0100 Subject: [PATCH 15/23] Proto: Convert sapling_apply_diff_cost to saturation arith Signed-off-by: Yann Regis-Gianas --- .../lib_protocol/sapling_storage.ml | 21 +++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/src/proto_alpha/lib_protocol/sapling_storage.ml b/src/proto_alpha/lib_protocol/sapling_storage.ml index 7e7c63106a7c..413c78c2a686 100644 --- a/src/proto_alpha/lib_protocol/sapling_storage.ml +++ b/src/proto_alpha/lib_protocol/sapling_storage.ml @@ -398,11 +398,21 @@ let init ctx id ~memo_size = (* Gas costs for apply_diff. *) let sapling_apply_diff_cost ~inputs ~outputs = - Z.add - (Z.of_int 1_300_000) - (Z.add - (Z.mul (Z.of_int inputs) (Z.of_int 5_000)) - (Z.mul (Z.of_int outputs) (Z.of_int 55_000))) + let open Saturation_repr in + let mul_safe_int x = + Option.bind (of_int_opt x) mul_safe + |> function + | None -> + (* Since you can read below that x is always less than 2147483648. *) + assert false + | Some x -> + x + in + add + (safe_int 1_300_000) + (add + (scale_fast (mul_safe_int 5_000) (safe_int inputs)) + (scale_fast (mul_safe_int 55_000) (safe_int outputs))) (** Applies a diff to a state id stored in the context. Updates Commitments, Ciphertexts and Nullifiers using the diff and updates the Roots using the @@ -413,7 +423,6 @@ let apply_diff ctx id diff = let nb_nullifiers = List.length diff.nullifiers in let sapling_cost = sapling_apply_diff_cost ~inputs:nb_nullifiers ~outputs:nb_commitments - |> Saturation_repr.of_z_opt |> Saturation_repr.saturate_if_undef in Raw_context.consume_gas ctx sapling_cost >>?= fun ctx -> -- GitLab From c6fb886d8120c479cae3b364df2f39fe236689c3 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Wed, 27 Jan 2021 18:51:20 +0100 Subject: [PATCH 16/23] Proto: Use safe_int when possible Signed-off-by: Yann Regis-Gianas --- src/proto_alpha/lib_protocol/script_interpreter.ml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/proto_alpha/lib_protocol/script_interpreter.ml b/src/proto_alpha/lib_protocol/script_interpreter.ml index e3cf135e2543..3c746e84e343 100644 --- a/src/proto_alpha/lib_protocol/script_interpreter.ml +++ b/src/proto_alpha/lib_protocol/script_interpreter.ml @@ -776,9 +776,7 @@ let rec step_bounded : (* The cost for this fold_left has been paid upfront *) let total_length = List.fold_left - (fun acc s -> - let len = S.of_int_opt (String.length s) |> S.saturate_if_undef in - S.add acc len) + (fun acc s -> S.add acc (S.safe_int (String.length s))) S.zero ss.elements in @@ -805,9 +803,7 @@ let rec step_bounded : (* The cost for this fold_left has been paid upfront *) let total_length = List.fold_left - (fun acc s -> - let len = S.of_int_opt (Bytes.length s) |> S.saturate_if_undef in - S.add acc len) + (fun acc s -> S.add acc (S.safe_int (Bytes.length s))) S.zero ss.elements in -- GitLab From 585914d9dbfc0592e2bf7cdaa1e9cd2ead70d717 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Wed, 27 Jan 2021 18:55:08 +0100 Subject: [PATCH 17/23] Proto: Remove redundant test, saturated integers are always non neg Signed-off-by: Yann Regis-Gianas --- src/proto_alpha/lib_protocol/script_repr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/proto_alpha/lib_protocol/script_repr.ml b/src/proto_alpha/lib_protocol/script_repr.ml index b271d116b8ec..d7fefc5a5483 100644 --- a/src/proto_alpha/lib_protocol/script_repr.ml +++ b/src/proto_alpha/lib_protocol/script_repr.ml @@ -134,7 +134,7 @@ let traversal_cost node = let cost_of_size (blocks, words) = let open Gas_limit_repr in - (S.max S.zero (S.sub blocks (S.safe_int 1)) *@ alloc_cost S.zero) + (S.sub blocks (S.safe_int 1) *@ alloc_cost S.zero) +@ alloc_cost words +@ step_cost blocks let cost_of_size_int pair = cost_of_size (convert_pair pair) -- GitLab From 91a3dbed0192e0189eb46137c3dba3eb842449a1 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Thu, 28 Jan 2021 09:10:46 +0100 Subject: [PATCH 18/23] Proto: Revamp a call to alloc_cost that disappeared in a refactoring Signed-off-by: Yann Regis-Gianas --- src/proto_alpha/lib_protocol/gas_limit_repr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.ml b/src/proto_alpha/lib_protocol/gas_limit_repr.ml index ded529d448d1..764fb97c55ca 100644 --- a/src/proto_alpha/lib_protocol/gas_limit_repr.ml +++ b/src/proto_alpha/lib_protocol/gas_limit_repr.ml @@ -215,7 +215,7 @@ let raw_consume gas_counter cost = let alloc_cost n = S.scale_fast allocation_weight S.(add n (safe_const_exn 1)) -let alloc_bytes_cost n = S.safe_int ((n + 7) / 8) +let alloc_bytes_cost n = alloc_cost (S.safe_int ((n + 7) / 8)) let atomic_step_cost : 'a S.t -> cost = S.may_saturate -- GitLab From 0fbed686289111ceffeb888c3ae1173f650ce3f5 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Mon, 1 Feb 2021 12:52:11 +0100 Subject: [PATCH 19/23] Proto: Simplify the definition of zero Signed-off-by: Yann Regis-Gianas --- src/proto_alpha/lib_protocol/gas_limit_repr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.ml b/src/proto_alpha/lib_protocol/gas_limit_repr.ml index 764fb97c55ca..89ac1db65496 100644 --- a/src/proto_alpha/lib_protocol/gas_limit_repr.ml +++ b/src/proto_alpha/lib_protocol/gas_limit_repr.ml @@ -76,7 +76,7 @@ module Arith = struct let add = S.add - let zero = S.(may_saturate zero) + let zero = S.zero let min = S.min -- GitLab From 3b4289cbd4c7f2191a30762f1a948c0e5273792f Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Mon, 1 Feb 2021 13:12:33 +0100 Subject: [PATCH 20/23] Proto: Add mul_safe_exn and mul_safe_of_int_exn in Saturation_repr Signed-off-by: Yann Regis-Gianas --- .../lib_protocol/gas_limit_repr.ml | 48 ++++--------------- .../lib_protocol/sapling_storage.ml | 13 +---- .../lib_protocol/saturation_repr.ml | 16 +++++++ .../lib_protocol/saturation_repr.mli | 18 +++++++ 4 files changed, 46 insertions(+), 49 deletions(-) diff --git a/src/proto_alpha/lib_protocol/gas_limit_repr.ml b/src/proto_alpha/lib_protocol/gas_limit_repr.ml index 89ac1db65496..406d62d1a245 100644 --- a/src/proto_alpha/lib_protocol/gas_limit_repr.ml +++ b/src/proto_alpha/lib_protocol/gas_limit_repr.ml @@ -31,37 +31,7 @@ type integral_tag module S = Saturation_repr -(* - - When a saturated integer is sufficiently small (i.e. strictly less - than 2147483648), we can assign it the type [mul_safe S.t] to use - it within fast multiplications, named [S.scale_fast] and - [S.mul_fast]. - - The following function allows such type assignment but may raise an - exception if the assumption is wrong. Therefore, [assert_mul_safe] - should only be used to define toplevel values, so that these - exceptions can only occur during startup. - -*) -let assert_mul_safe_exn x = - match S.mul_safe x with None -> assert false | Some x -> x - -(* - - Similarly as [assert_mul_safe_exn], [safe_const_exn] must only be applied - to integer literals that are small enough for fast multiplications. - -*) -let safe_const_exn x = - match S.of_int_opt x with - | None -> - (* Since [safe_const_exn] is only applied to small integers: *) - assert false - | Some x -> - assert_mul_safe_exn x - -let scaling_factor = safe_const_exn 1000 +let scaling_factor = S.mul_safe_of_int_exn 1000 module Arith = struct type 'a t = S.may_saturate S.t @@ -191,21 +161,21 @@ let cost_encoding = S.z_encoding let pp_cost fmt z = S.pp fmt z let allocation_weight = - S.(mul_fast scaling_factor (safe_const_exn 2)) |> assert_mul_safe_exn + S.(mul_fast scaling_factor (S.mul_safe_of_int_exn 2)) |> S.mul_safe_exn let step_weight = scaling_factor let read_base_weight = - S.(mul_fast scaling_factor (safe_const_exn 100)) |> assert_mul_safe_exn + S.(mul_fast scaling_factor (S.mul_safe_of_int_exn 100)) |> S.mul_safe_exn let write_base_weight = - S.(mul_fast scaling_factor (safe_const_exn 160)) |> assert_mul_safe_exn + S.(mul_fast scaling_factor (S.mul_safe_of_int_exn 160)) |> S.mul_safe_exn let byte_read_weight = - S.(mul_fast scaling_factor (safe_const_exn 10)) |> assert_mul_safe_exn + S.(mul_fast scaling_factor (S.mul_safe_of_int_exn 10)) |> S.mul_safe_exn let byte_written_weight = - S.(mul_fast scaling_factor (safe_const_exn 15)) |> assert_mul_safe_exn + S.(mul_fast scaling_factor (S.mul_safe_of_int_exn 15)) |> S.mul_safe_exn let cost_to_milligas (cost : cost) : Arith.fp = cost @@ -213,7 +183,8 @@ let raw_consume gas_counter cost = let gas = cost_to_milligas cost in Arith.sub_opt gas_counter gas -let alloc_cost n = S.scale_fast allocation_weight S.(add n (safe_const_exn 1)) +let alloc_cost n = + S.scale_fast allocation_weight S.(add n (S.mul_safe_of_int_exn 1)) let alloc_bytes_cost n = alloc_cost (S.safe_int ((n + 7) / 8)) @@ -233,4 +204,5 @@ let ( +@ ) x y = S.add x y let ( *@ ) x y = S.mul x y -let alloc_mbytes_cost n = alloc_cost (safe_const_exn 12) +@ alloc_bytes_cost n +let alloc_mbytes_cost n = + alloc_cost (S.mul_safe_of_int_exn 12) +@ alloc_bytes_cost n diff --git a/src/proto_alpha/lib_protocol/sapling_storage.ml b/src/proto_alpha/lib_protocol/sapling_storage.ml index 413c78c2a686..8e2e57aff350 100644 --- a/src/proto_alpha/lib_protocol/sapling_storage.ml +++ b/src/proto_alpha/lib_protocol/sapling_storage.ml @@ -399,20 +399,11 @@ let init ctx id ~memo_size = (* Gas costs for apply_diff. *) let sapling_apply_diff_cost ~inputs ~outputs = let open Saturation_repr in - let mul_safe_int x = - Option.bind (of_int_opt x) mul_safe - |> function - | None -> - (* Since you can read below that x is always less than 2147483648. *) - assert false - | Some x -> - x - in add (safe_int 1_300_000) (add - (scale_fast (mul_safe_int 5_000) (safe_int inputs)) - (scale_fast (mul_safe_int 55_000) (safe_int outputs))) + (scale_fast (mul_safe_of_int_exn 5_000) (safe_int inputs)) + (scale_fast (mul_safe_of_int_exn 55_000) (safe_int outputs))) (** Applies a diff to a state id stored in the context. Updates Commitments, Ciphertexts and Nullifiers using the diff and updates the Roots using the diff --git a/src/proto_alpha/lib_protocol/saturation_repr.ml b/src/proto_alpha/lib_protocol/saturation_repr.ml index 7db5dcd4c915..55f244a62fa7 100644 --- a/src/proto_alpha/lib_protocol/saturation_repr.ml +++ b/src/proto_alpha/lib_protocol/saturation_repr.ml @@ -78,6 +78,22 @@ let small_enough z = let mul_safe x = if small_enough x then Some x else None +let mul_safe_exn x = + match mul_safe x with + | None -> + failwith (Format.sprintf "mul_safe_exn: %d must be below 2147483648" x) + | Some x -> + x + +let mul_safe_of_int_exn x = + Option.bind (of_int_opt x) mul_safe + |> function + | None -> + failwith + (Format.sprintf "mul_safe_of_int_exn: %d must be below 2147483648" x) + | Some x -> + x + (* If [x] is positive, shifting to the right will produce a number which is positive and is less than [x]. *) let shift_right x y = (x :> int) lsr y diff --git a/src/proto_alpha/lib_protocol/saturation_repr.mli b/src/proto_alpha/lib_protocol/saturation_repr.mli index 53101f12ecaa..0e05efe44d66 100644 --- a/src/proto_alpha/lib_protocol/saturation_repr.mli +++ b/src/proto_alpha/lib_protocol/saturation_repr.mli @@ -155,6 +155,24 @@ val of_int_opt : int -> may_saturate t option and [None] otherwise. *) val of_z_opt : Z.t -> may_saturate t option +(** When a saturated integer is sufficiently small (i.e. strictly less + than 2147483648), we can assign it the type [mul_safe S.t] to use + it within fast multiplications, named [S.scale_fast] and + [S.mul_fast]. + + The following function allows such type assignment but may raise an + exception if the assumption is wrong. Therefore, [mul_safe_exn] + should only be used to define toplevel values, so that these + exceptions can only occur during startup. + *) +val mul_safe_exn : may_saturate t -> mul_safe t + +(** [mul_safe_of_int_exn x] is the composition of [of_int_opt] and + [mul_safe] in the option monad. This function raises [Invalid_argument] + if [x] is not safe. This function should be used on integer literals + that are obviously [mul_safe]. *) +val mul_safe_of_int_exn : int -> mul_safe t + (** [saturate_if_undef o] is [saturated] if [o] is [None] and [x] if [o = Some x]. *) val saturate_if_undef : may_saturate t option -> may_saturate t -- GitLab From ef96390275f8948e7c209453fdd6e46df235fc80 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Mon, 1 Feb 2021 13:13:29 +0100 Subject: [PATCH 21/23] Proto: Do not export [saturate_if_undef] Signed-off-by: Yann Regis-Gianas --- src/proto_alpha/lib_protocol/saturation_repr.mli | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/proto_alpha/lib_protocol/saturation_repr.mli b/src/proto_alpha/lib_protocol/saturation_repr.mli index 0e05efe44d66..4ef8539ef8c5 100644 --- a/src/proto_alpha/lib_protocol/saturation_repr.mli +++ b/src/proto_alpha/lib_protocol/saturation_repr.mli @@ -173,10 +173,6 @@ val mul_safe_exn : may_saturate t -> mul_safe t that are obviously [mul_safe]. *) val mul_safe_of_int_exn : int -> mul_safe t -(** [saturate_if_undef o] is [saturated] if [o] is [None] and [x] if [o = Some - x]. *) -val saturate_if_undef : may_saturate t option -> may_saturate t - (** [safe_int x] is [of_int_opt x |> saturate_if_undef]. *) val safe_int : int -> may_saturate t -- GitLab From d3ae32833e7d8f278dd94017e0c7de580b7bb6e5 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Mon, 1 Feb 2021 16:49:20 +0100 Subject: [PATCH 22/23] Proto: Simplify the implementation of mul_safe_exn Signed-off-by: Yann Regis-Gianas --- src/proto_alpha/lib_protocol/saturation_repr.ml | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/proto_alpha/lib_protocol/saturation_repr.ml b/src/proto_alpha/lib_protocol/saturation_repr.ml index 55f244a62fa7..a09c3e5c8519 100644 --- a/src/proto_alpha/lib_protocol/saturation_repr.ml +++ b/src/proto_alpha/lib_protocol/saturation_repr.ml @@ -79,11 +79,8 @@ let small_enough z = let mul_safe x = if small_enough x then Some x else None let mul_safe_exn x = - match mul_safe x with - | None -> - failwith (Format.sprintf "mul_safe_exn: %d must be below 2147483648" x) - | Some x -> - x + if small_enough x then x + else failwith (Format.sprintf "mul_safe_exn: %d must be below 2147483648" x) let mul_safe_of_int_exn x = Option.bind (of_int_opt x) mul_safe -- GitLab From 75e3b77f8da533a73b36cda88c856371d5c0d305 Mon Sep 17 00:00:00 2001 From: Yann Regis-Gianas Date: Thu, 4 Feb 2021 17:10:58 +0100 Subject: [PATCH 23/23] Remove dead code --- .../lib_protocol/test/saturation.ml | 109 ------------------ 1 file changed, 109 deletions(-) delete mode 100644 src/proto_alpha/lib_protocol/test/saturation.ml diff --git a/src/proto_alpha/lib_protocol/test/saturation.ml b/src/proto_alpha/lib_protocol/test/saturation.ml deleted file mode 100644 index 427c3c73cd2f..000000000000 --- a/src/proto_alpha/lib_protocol/test/saturation.ml +++ /dev/null @@ -1,109 +0,0 @@ -(*****************************************************************************) -(* *) -(* Open Source License *) -(* Copyright (c) 2020 Nomadic Labs, *) -(* *) -(* Permission is hereby granted, free of charge, to any person obtaining a *) -(* copy of this software and associated documentation files (the "Software"),*) -(* to deal in the Software without restriction, including without limitation *) -(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *) -(* and/or sell copies of the Software, and to permit persons to whom the *) -(* Software is furnished to do so, subject to the following conditions: *) -(* *) -(* The above copyright notice and this permission notice shall be included *) -(* in all copies or substantial portions of the Software. *) -(* *) -(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*) -(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *) -(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *) -(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*) -(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *) -(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *) -(* DEALINGS IN THE SOFTWARE. *) -(* *) -(*****************************************************************************) - -open Protocol - -let valid (z : _ Saturation_repr.t) = - let x = z |> Saturation_repr.to_int in - x >= 0 && x < max_int - -open Saturation_repr - -exception Saturating_test_error of string - -let err x = Exn (Saturating_test_error x) - -let small_enough (z : _ t) = - Compare.Int.((z |> to_int) land 0x7fffffff80000000 = 0) - -let n = safe_int 123123 - -let m = safe_int 377337 - -let shift_right () = - fail_unless - (shift_right saturated 63 = safe_int 0) - (err "saturated lsr 63 = 0") - >>=? fun () -> - fail_unless (shift_right (safe_int 1) 63 = safe_int 0) (err "1 lsr 63 = 0") - >>=? fun () -> - fail_unless (shift_right (safe_int 1) 0 = safe_int 1) (err "1 lsr 0 = 1") - >>=? fun () -> - fail_unless (shift_right (safe_int 0) 63 = safe_int 0) (err "0 lsr 63 = 0") - -let add () = - fail_unless - (add saturated (safe_int 1) = saturated) - (err "saturated + 1 <> saturated") - >>=? fun () -> - fail_unless (add zero n = n) (err "zero + n = n") - >>=? fun () -> - fail_unless (add n zero = n) (err "n + zero = n") - >>=? fun () -> - let r = add n m in - fail_unless - (valid r && r = safe_int ((n :> int) + (m :> int))) - (err "add does not behave like + on small numbers.") - -let sub () = - fail_unless (sub zero n = zero) (err "zero - n <> zero") - >>=? fun () -> - let n = max n m and m = min n m in - let r = sub n m in - fail_unless - (valid r && r = safe_int ((n :> int) - (m :> int))) - (err "sub does not behave like - on small numbers.") - -let mul () = - fail_unless - (mul saturated saturated = saturated) - (err "saturated * saturated <> saturated") - >>=? fun () -> - fail_unless (mul zero saturated = zero) (err "zero * saturated <> zero") - >>=? fun () -> - fail_unless (mul saturated zero = zero) (err "saturated * zero <> zero") - >>=? fun () -> - let max_squared = safe_int (1 lsl 31) in - let r = mul max_squared max_squared in - fail_unless - (valid r && r = saturated) - (err "2 ^ 31 * 2 ^ 31 should be saturated") - >>=? fun () -> - let safe_squared = safe_int ((1 lsl 31) - 1) in - let r = mul safe_squared safe_squared in - fail_unless - (valid r && r <> saturated) - (err "(2 ^ 31 - 1) * (2 ^ 31 - 1) should not be saturated") - >>=? fun () -> - let r = mul n m in - fail_unless - (valid r && r = safe_int ((n |> to_int) * (m |> to_int))) - (err "mul does not behave like * on small numbers.") - -let tests = - [ Test.tztest "Shift right" `Quick shift_right; - Test.tztest "Addition" `Quick add; - Test.tztest "Subtraction" `Quick sub; - Test.tztest "Multiplication" `Quick mul ] -- GitLab