saturation_repr.mli
(*****************************************************************************)
(* *)
(* Open Source License *)
(* Copyright (c) 2020 Nomadic Labs, <contact@nomadic-labs.com> *)
(* *)
(* 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. *)
(* *)
(*****************************************************************************)
(** This module provides saturated arithmetic between 0 and 2^62 - 1.
This means that the arithmetic operations provided by this module
do not overflow. If an operation would produce an integer [x]
greater than [2 ^ 62 - 1], it is [saturated] to this
value. Similarly, if an operation would produce a negative integer,
it outputs [zero] instead.
This saturation arithmetic is used to monitor gas levels. While the
gas model can produce values beyond 2^62 - 1, there is no point in
distinguishing these values from 2^62 - 1 because the amount of gas
available is significantly lower than this limit.
Notice that most saturation arithmetic operations do not behave
as their standard counterparts when one of their operands is
saturated. For instance,
(saturated + saturated) - saturated = 0
For more information about saturation arithmetic, take a look at:
https://en.wikipedia.org/wiki/Saturation_arithmetic
*)
(** An integer of type ['a t] is between [0] and [saturated].
The type parameter ['a] is [mul_safe] if the integer is known
not to overflow when multiplied with another [mul_safe t].
The type parameter ['a] is [may_saturate] if the integer is
not known to be sufficiently small to prevent overflow during
multiplication.
*)
type 'a t = private int
type mul_safe
type may_saturate
val may_saturate : _ t -> may_saturate t
(** [to_int x] returns the underlying integer representing [x]. *)
val to_int : 'a t -> int
(** 0 *)
val zero : _ t
(** 1 *)
val one : _ t
(** 2^62 - 1 *)
val saturated : may_saturate t
(** We inherit the order over native integers. *)
val ( >= ) : _ t -> _ t -> bool
val ( > ) : _ t -> _ t -> bool
val ( <= ) : _ t -> _ t -> bool
val ( < ) : _ t -> _ t -> bool
val ( = ) : _ t -> _ t -> bool
val ( <> ) : _ t -> _ t -> bool
val equal : _ t -> _ t -> bool
val min : 'a t -> 'a t -> 'a t
val max : 'a t -> 'a t -> 'a t
val compare : 'a t -> 'b t -> int
(** [a >! b] is [a > b]. Avoids using [to_int]. *)
val ( >! ) : _ t -> int -> bool
(** [numbits x] returns the number of bits used in the binary representation
of [x]. *)
val numbits : 'a 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
(** [shift_left x y] behaves like a logical shift of [x] by [y] bits
to the left. [y] must be between 0 and 63. In cases where [x lsl y]
is overflowing, [shift_left x y] is [saturated]. *)
val shift_left : '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]. *)
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]. 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
provoke overflows during multiplication to perform a mere
multiplication. *)
val mul_fast : mul_safe t -> mul_safe t -> may_saturate t
(** [scale_fast x y] exploits the fact that [x] is known not to
provoke overflows during multiplication to perform a
multiplication faster than [mul]. *)
val scale_fast : mul_safe t -> _ t -> may_saturate t
(** [add x y] behaves like addition between native integers as long as
its result stay below [saturated]. Otherwise, [add] returns
[saturated]. *)
val add : _ t -> _ t -> may_saturate t
(** [succ x] is like [add one x] *)
val succ : _ t -> may_saturate t
(** [sub x y] behaves like subtraction between native integers as long
as its result stay positive. Otherwise, [sub] returns [zero].
This function assumes that [x] is not saturated.
*)
val sub : 'a t -> _ t -> 'a t
(** [sub_opt x y] behaves like subtraction between native integers as
long as its result stay positive. Otherwise, [sub] returns
[None]. *)
val sub_opt : 'a t -> _ t -> 'a t option
(** [ediv x y] returns [x / y]. This operation never saturates, hence
it is exactly the same as its native counterpart. [y] is supposed
to be strictly greater than 0, otherwise this function raises
[Division_by_zero]. *)
val ediv : 'a t -> _ t -> 'a t
(** [erem x y] returns [x mod y]. [y] is supposed to be strictly
greater than 0, otherwise this function raises
[Division_by_zero]. *)
val erem : _ t -> 'b t -> 'b t
(** [sqrt x] returns the square root of x, rounded down. *)
val sqrt : _ t -> 'a t
(** [of_int_opt x] returns [Some x] if [x >= 0] and [x < saturated],
and [None] otherwise. *)
val of_int_opt : int -> may_saturate t option
(** [of_z_opt x] returns [Some x] if [x >= 0] and [x < saturated],
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
(** [safe_z z] is [of_z_opt x |> saturate_if_undef]. *)
val safe_z : Z.t -> 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
(** Encoding for [t] through the encoding for [z] integers. *)
val z_encoding : _ t Data_encoding.t
(** Encoding for [t] through the encoding for non-negative integers. *)
val n_encoding : _ t Data_encoding.t
(** A pretty-printer for native integers. *)
val pp : Format.formatter -> _ t -> unit
(** Syntax for simple representations. *)
module Syntax : sig
val log2 : _ t -> may_saturate t
val sqrt : _ t -> may_saturate t
val ( + ) : _ t -> _ t -> may_saturate t
val ( - ) : _ t -> _ t -> may_saturate t
val ( * ) : _ t -> _ t -> may_saturate t
val ( < ) : _ t -> _ t -> bool
val ( = ) : _ t -> _ t -> bool
val ( lsr ) : 'a t -> int -> 'a t
val ( lsl ) : 'a t -> int -> 'a t
end