mutnet 0.7.0

Unsafe-free and allocation-free, no-std network protocol parsing and in-place manipulation library.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37

use super::*;

const CHECKSUM_INPUT_LENGTH: usize = 64;

#[kani::proof]
fn finalize_checksum_proof() {
    finalize_checksum(kani::any());
}

#[kani::proof]
fn internet_checksum_up_to_64_bytes_proof() {
    let mut any_array: [u8; CHECKSUM_INPUT_LENGTH] = kani::any();
    let any_slice_length = kani::any_where(|i| *i <= CHECKSUM_INPUT_LENGTH);
    let any_slice = &mut any_array[..any_slice_length];

    internet_checksum_up_to_64_bytes(any_slice);
}

#[kani::proof]
#[kani::unwind(20)]
fn internet_checksum_intermediary_proof() {
    let mut any_array: [u8; CHECKSUM_INPUT_LENGTH] = kani::any();
    let any_slice_length = kani::any_where(|i| *i <= CHECKSUM_INPUT_LENGTH);
    let any_slice = &mut any_array[..any_slice_length];

    internet_checksum_intermediary::<4>(any_slice);
}

#[kani::proof]
#[kani::unwind(20)]
fn internet_checksum_variable_chunks_proof() {
    let mut any_array: [u8; CHECKSUM_INPUT_LENGTH] = kani::any();
    let any_slice_length = kani::any_where(|i| *i <= CHECKSUM_INPUT_LENGTH);
    let any_slice = &mut any_array[..any_slice_length];

    internet_checksum::<4>(0, any_slice);
}