Legend:
Library
Module
Module type
Parameter
Class
Class type
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:
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.
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.
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.
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.
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.
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.