# Checked Arithmetics

When working with data from an unknown source, it is often useful to be able to perform "checked arithmetics" to avoid overflows in computations. A common example is when computing the size of a buffer:

    void createImage(Nat width, Nat height) {
        Nat size = width * height * 4;
        Buffer buffer = buffer(size);
        // Index into 'buffer'...
    }

However, if `width` and `height` are too large the multiplication will overflow, causing the allocation to be too small. As such, subsequent accesses into the buffer may be out of bounds (note that accesses to `buffer` are checked, so nothing bad will happen unless you access the buffer from machine code).

In these cases, one would need to check that none of the multiplications overflow. This is tedious to do, and not easy to get right. To help, the Storm standard library provides `core.CheckedNat` and `core.CheckedWord`. Both behave like a (simplified version of) `core.Nat` and `core.Word` respectively. The difference is that all arithmetic operations are checked for overflow. When this happen, they turn into a special "error" value, that makes any further calculations fail. The error value is thereby propagated to the end without having to check for errors at each step.

Other numbers can be automatically converted to `core.CheckedNat` and `core.CheckedWord` respectively. Thereby, as soon as one value in an expression is a checked value, the other ones will be converted accordingly as well (given the proper evaluation order). For example, the `createImage` function can be rewritten as follows to avoid overflows:

    void createImage(Nat width, Nat height) {
        CheckedNat size = CheckedNat(width) * CheckedNat(height) * 4;
        unless (value = size.nat)
            fail "Integer overflow!";
        Buffer buffer = buffer(size);
        // Index into 'buffer'...
    }

As can be noted above, the `nat` member is used to convert the checked version to a normal `Nat`. This function returns a `Maybe<Nat>` that needs to be checked in a weak cast. It is also possible to check whether an error has occurred using `error`.