feat: formal verification of unsafe blocks

[remimimimimi]

This PR formally verifies of almost all unsafe blocks in code base. Related to #18. Covered unsafe blocks are correct in the sense described below.

Kani provides bit-precise bounded model checking of the given functions. This roughly means that it can prove that some assertion holds for all possible (bounded) cases. In particular, it can spot

1. out-of-bounds accesses,
2. actually-unsafe dereferencing of a raw pointer to invalid memory,
3. a division by zero error and an overflowing addition.

See limitations for things that Kani can not deal with.

Proofs for debug_expect_unchecked and FrozenCopyMap are omitted due to enormous resources needed for checking. The most resource heavy correctness proof of Mapping takes around 40GB of RAM.

Here's the last lines of the output of /usr/bin/time -v cargo kani:

Manual Harness Summary:
Complete - 7 successfully verified harnesses, 0 failures, 7 total.
        Command being timed: "cargo kani"
        User time (seconds): 999.49
        System time (seconds): 54.18
        Percent of CPU this job got: 99%
        Elapsed (wall clock) time (h:mm:ss or m:ss): 17:38.93
        Average shared text size (kbytes): 0
        Average unshared data size (kbytes): 0
        Average stack size (kbytes): 0
        Average total size (kbytes): 0
        Maximum resident set size (kbytes): 31144928
        Average resident set size (kbytes): 0
        Major (requiring I/O) page faults: 3
        Minor (reclaiming a frame) page faults: 41407989
        Voluntary context switches: 88457
        Involuntary context switches: 7903
        Swaps: 0
        File system inputs: 1056
        File system outputs: 2424552
        Socket messages sent: 0
        Socket messages received: 0
        Signals delivered: 0
        Page size (bytes): 4096
        Exit status: 0