Checks that are proved are dropped

The problem: Safety checks cost time: an index check on every access, an overflow check on every +.
An example: A loop that reads xs[i] for every i from 0 up to xs.len(). The check on each read can never fail.
What Nikaia checks: Nikaia keeps the checks, and drops one only where it has proved it cannot fail. remove-bounds-checks:on writes an index without its check where the compiler has proved 0 <= i < xs.len(). remove-overflow-checks:on does the same for a +, - or * whose result stays inside its type. A check that is not proved is not dropped.
The limit: Both are off by default: you ask for them in nikaia.toml. What is proved does not depend on them; they only choose what is written.

Go deeper