# Panic freedom

Let's start with a simple example: a function that squares a `u8`

integer. To extract this function to F* using hax, we simply need to
run the command `cargo hax into fstar`

in the directory of the crate
in which the function `square`

is defined.

*Note: throughout this tutorial, you can inspect the hax extraction to
F* for each code Rust snippets, by clicking on the "F* extraction"
tab.*

```
fn square(x: u8) -> u8 {
x * x
}
```

```
let square (x: u8) : u8 = x *! x
```

Though, if we try to verify this function, F* is complaining about a
subtyping issue: F* tells us that it is not able to prove that the
result of the multiplication `x * x`

fits the range of `u8`

. The
multiplication `x * x`

might indeed be overflowing!

For instance, running `square(16)`

panics: `16 * 16`

is `256`

, which
is just over `255`

, the largest integer that fits `u8`

. Rust does not
ensure that functions are *total*: a function might panic at any
point, or might never terminate.

## Rust and panicking code

Quoting the chapter To `panic!`

or Not to
`panic!`

from the Rust book:

The

`panic!`

macro signals that your program is in a state it can't handle and lets you tell the process to stop instead of trying to proceed with invalid or incorrect values.

A Rust program should panics only in a situation where an assumption
or an invariant is broken: a panics models an *invalid* state. Formal
verification is about proving such invalid state cannot occur, at all.

From this observation emerges the urge of proving Rust programs to be panic-free!

## Fixing our squaring function

Let's come back to our example. There is an informal assumption to the multiplication operator in Rust: the inputs should be small enough so that the addition doesn't overflow.

Note that Rust also provides `wrapping_mul`

, a non-panicking variant
of the multiplication on `u8`

that wraps when the result is bigger
than `255`

. Replacing the common multiplication with `wrapping_mul`

in
`square`

would fix the panic, but then, `square(256)`

returns zero.
Semantically, this is not what one would expect from `square`

.

Our problem is that our function `square`

is well-defined only when
its input is within `0`

and `15`

.

### Solution A: reflect the partialness of the function in Rust

A first solution is to make `square`

return an `Option<u8>`

instead of a `u8`

:

```
fn square_option(x: u8) -> Option<u8> {
if x >= 16 {
None
} else {
Some(x * x)
}
}
```

```
let square_option (x: u8) : Core.Option.t_Option u8 =
if x >=. 16uy
then Core.Option.Option_None <: Core.Option.t_Option u8
else Core.Option.Option_Some (x *! x) <: Core.Option.t_Option u8
```

Here, F* is able to prove panic-freedom: calling `square`

with any
input is safe. Though, one may argue that `square`

's input being small
enough should really be an assumption. Having to deal with the
possible integer overflowing whenever squaring is a huge burden. Can
we do better?

### Solution B: add a precondition

The type system of Rust doesn't allow the programmer to formalize the
assumption that `square`

expects a small `u8`

. This becomes
possible using hax: one can annotate a function with a pre-condition
on its inputs.

The pre-conditions and post-conditions on a function form a
*contract*: "if you give me some inputs that satisfies a given formula
(*the precondition*), I will produce a return value that satisfy
another formula (*the postcondition*)". Outside this contracts,
anything might happen: the function might panic, might run forever,
erase your disk, or anything.

The helper crate
hax-lib-macros
provdes the `requires`

proc-macro
which lets user writting pre-conditions directly in Rust.

```
#[hax_lib::requires(x < 16)]
fn square_requires(x: u8) -> u8 {
x * x
}
```

```
let square_requires (x: u8)
: Pure u8 (requires x <. 16uy) (requires fun _ -> True)
= x *! x
```

With this precondition, F* is able to prove panic freedom. From now
on, it is the responsability of the clients of `square`

to respect the
contact. The next step is thus be to verify, through hax extraction,
that `square`

is used correctly at every call site.

## Common panicking situations

Mutipication is not the only panicking function provided by the Rust library: most of the other integer arithmetic operation have such informal assumptions.

Another source of panics is indexing. Indexing in an array, a slice or a vector is a partial operation: the index might be out of range.

In the example folder of hax, you can find the `chacha20`

example
that makes use of pre-conditions to prove panic freedom.

Another solution for safe indexing is to use the newtype index pattern, which is also supported by hax. The data invariants chapter gives more details about this.