Module Mavryk_raw_protocol_001_PtAtLas.Saturation_repr

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

type 'a t = private int

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 mul_safe
type may_saturate
val may_saturate : _ t -> may_saturate t
val to_int : 'a t -> int

to_int x returns the underlying integer representing x.

val zero : _ t

0

val one : _ t

1

val saturated : may_saturate t

2^62 - 1

val (>=) : _ t -> _ t -> bool

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 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
val (>!) : _ t -> int -> bool

a >! b is a > b. Avoids using to_int.

val numbits : 'a t -> int

numbits x returns the number of bits used in the binary representation of x.

val shift_right : 'a t -> int -> 'a t

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_left : '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 mul : _ t -> _ t -> may_saturate t

mul x y behaves like multiplication between native integers as long as its result stay below saturated. Otherwise, mul returns saturated.

val mul_safe : _ t -> mul_safe t option

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_fast : mul_safe t -> mul_safe t -> may_saturate t

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 scale_fast : mul_safe t -> _ 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 add : _ 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 succ : _ t -> may_saturate t

succ x is like add one x

val sub : 'a t -> _ t -> 'a 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_opt : 'a t -> _ t -> 'a t option

sub_opt x y behaves like subtraction between native integers as long as its result stay positive. Otherwise, sub returns None.

val ediv : 'a t -> _ t -> 'a t

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 erem : _ t -> 'b t -> 'b 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 sqrt : _ t -> 'a t

sqrt x returns the square root of x, rounded down.

val of_int_opt : int -> may_saturate t option

of_int_opt x returns Some x if x >= 0 and x < saturated, and None otherwise.

of_z_opt x returns Some x if x >= 0 and x < saturated, and None otherwise.

val mul_safe_exn : may_saturate t -> mul_safe t

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_of_int_exn : int -> 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.

safe_z z is of_z_opt x |> saturate_if_undef.

val safe_int : int -> may_saturate t

safe_int x is of_int_opt x |> saturate_if_undef.

to_z z is Z.of_int.

Encoding for t through the encoding for z integers.

Encoding for t through the encoding for non-negative integers.

A pretty-printer for native integers.

module Syntax : sig ... end

Syntax for simple representations.