Skip to content

Commit

Permalink
Switch proofs from any_vec to slices
Browse files Browse the repository at this point in the history
  • Loading branch information
@arctic-alpaca
arctic-alpaca committed Sep 25, 2023
1 parent b7eb10c commit b80b788
Show file tree
Hide file tree
Showing 8 changed files with 807 additions and 629 deletions.
76 changes: 41 additions & 35 deletions src/arp/verification.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,13 @@ const HEADROOM: usize = SLICE_LENGTH + 10;

#[kani::proof]
fn get_arp_proof() {
let vec = kani::vec::any_vec::<u8, SLICE_LENGTH>();
let slice = vec.as_slice();
let headroom = kani::any();
kani::assume(headroom < HEADROOM);
let mut any_array: [u8; SLICE_LENGTH] = kani::any();
let any_slice_length = kani::any_where(|i| *i <= SLICE_LENGTH);
let any_slice = &mut any_array[..any_slice_length];

if let Ok(to_test) = DataBuffer::<_, Eth>::new(slice, headroom) {
let any_headroom = kani::any_where(|i| *i <= HEADROOM);

if let Ok(to_test) = DataBuffer::<_, Eth>::new(any_slice, any_headroom) {
if let Ok(to_test) = DataBuffer::<_, Arp<Eth>>::new_from_lower(to_test) {
let _ = to_test.arp_hardware_type();
let _ = to_test.arp_protocol_type();
Expand All @@ -31,16 +32,17 @@ fn get_arp_proof() {

#[kani::proof]
fn arp_set_operation_code_proof() {
let mut vec = kani::vec::any_vec::<u8, SLICE_LENGTH>();
let slice = vec.as_mut_slice();
let headroom = kani::any();
kani::assume(headroom < HEADROOM);
let mut any_array: [u8; SLICE_LENGTH] = kani::any();
let any_slice_length = kani::any_where(|i| *i <= SLICE_LENGTH);
let any_slice = &mut any_array[..any_slice_length];

let any_headroom = kani::any_where(|i| *i <= HEADROOM);

if let Ok(to_test) = DataBuffer::<_, Eth>::new(slice, headroom) {
if let Ok(to_test) = DataBuffer::<_, Eth>::new(any_slice, any_headroom) {
if let Ok(mut to_test) = DataBuffer::<_, Arp<Eth>>::new_from_lower(to_test) {
to_test.arp_set_operation_code(kani::any());
let _ = DataBuffer::<_, Arp<Eth>>::new_from_lower(
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), headroom).unwrap(),
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), any_headroom).unwrap(),
)
.unwrap();
}
Expand All @@ -49,16 +51,17 @@ fn arp_set_operation_code_proof() {

#[kani::proof]
fn arp_set_sender_hardware_address_proof() {
let mut vec = kani::vec::any_vec::<u8, SLICE_LENGTH>();
let slice = vec.as_mut_slice();
let headroom = kani::any();
kani::assume(headroom < HEADROOM);
let mut any_array: [u8; SLICE_LENGTH] = kani::any();
let any_slice_length = kani::any_where(|i| *i <= SLICE_LENGTH);
let any_slice = &mut any_array[..any_slice_length];

let any_headroom = kani::any_where(|i| *i <= HEADROOM);

if let Ok(to_test) = DataBuffer::<_, Eth>::new(slice, headroom) {
if let Ok(to_test) = DataBuffer::<_, Eth>::new(any_slice, any_headroom) {
if let Ok(mut to_test) = DataBuffer::<_, Arp<Eth>>::new_from_lower(to_test) {
to_test.arp_set_sender_hardware_address(&kani::any());
let _ = DataBuffer::<_, Arp<Eth>>::new_from_lower(
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), headroom).unwrap(),
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), any_headroom).unwrap(),
)
.unwrap();
}
Expand All @@ -67,16 +70,17 @@ fn arp_set_sender_hardware_address_proof() {

#[kani::proof]
fn arp_set_sender_protocol_address_proof() {
let mut vec = kani::vec::any_vec::<u8, SLICE_LENGTH>();
let slice = vec.as_mut_slice();
let headroom = kani::any();
kani::assume(headroom < HEADROOM);
let mut any_array: [u8; SLICE_LENGTH] = kani::any();
let any_slice_length = kani::any_where(|i| *i <= SLICE_LENGTH);
let any_slice = &mut any_array[..any_slice_length];

if let Ok(to_test) = DataBuffer::<_, Eth>::new(slice, headroom) {
let any_headroom = kani::any_where(|i| *i <= HEADROOM);

if let Ok(to_test) = DataBuffer::<_, Eth>::new(any_slice, any_headroom) {
if let Ok(mut to_test) = DataBuffer::<_, Arp<Eth>>::new_from_lower(to_test) {
to_test.arp_set_sender_protocol_address(&kani::any());
let _ = DataBuffer::<_, Arp<Eth>>::new_from_lower(
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), headroom).unwrap(),
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), any_headroom).unwrap(),
)
.unwrap();
}
Expand All @@ -85,16 +89,17 @@ fn arp_set_sender_protocol_address_proof() {

#[kani::proof]
fn arp_set_target_hardware_address_proof() {
let mut vec = kani::vec::any_vec::<u8, SLICE_LENGTH>();
let slice = vec.as_mut_slice();
let headroom = kani::any();
kani::assume(headroom < HEADROOM);
let mut any_array: [u8; SLICE_LENGTH] = kani::any();
let any_slice_length = kani::any_where(|i| *i <= SLICE_LENGTH);
let any_slice = &mut any_array[..any_slice_length];

let any_headroom = kani::any_where(|i| *i <= HEADROOM);

if let Ok(to_test) = DataBuffer::<_, Eth>::new(slice, headroom) {
if let Ok(to_test) = DataBuffer::<_, Eth>::new(any_slice, any_headroom) {
if let Ok(mut to_test) = DataBuffer::<_, Arp<Eth>>::new_from_lower(to_test) {
to_test.arp_set_target_hardware_address(&kani::any());
let _ = DataBuffer::<_, Arp<Eth>>::new_from_lower(
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), headroom).unwrap(),
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), any_headroom).unwrap(),
)
.unwrap();
}
Expand All @@ -103,16 +108,17 @@ fn arp_set_target_hardware_address_proof() {

#[kani::proof]
fn arp_set_target_protocol_address_proof() {
let mut vec = kani::vec::any_vec::<u8, SLICE_LENGTH>();
let slice = vec.as_mut_slice();
let headroom = kani::any();
kani::assume(headroom < HEADROOM);
let mut any_array: [u8; SLICE_LENGTH] = kani::any();
let any_slice_length = kani::any_where(|i| *i <= SLICE_LENGTH);
let any_slice = &mut any_array[..any_slice_length];

let any_headroom = kani::any_where(|i| *i <= HEADROOM);

if let Ok(to_test) = DataBuffer::<_, Eth>::new(slice, headroom) {
if let Ok(to_test) = DataBuffer::<_, Eth>::new(any_slice, any_headroom) {
if let Ok(mut to_test) = DataBuffer::<_, Arp<Eth>>::new_from_lower(to_test) {
to_test.arp_set_target_protocol_address(&kani::any());
let _ = DataBuffer::<_, Arp<Eth>>::new_from_lower(
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), headroom).unwrap(),
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), any_headroom).unwrap(),
)
.unwrap();
}
Expand Down
26 changes: 17 additions & 9 deletions src/checksum/verification.rs
View file
Original file line number Diff line number Diff line change
@@ -1,29 +1,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 vec = kani::vec::any_vec::<u8, 64>();
let slice = vec.as_slice();
internet_checksum_up_to_64_bytes(slice);
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 vec = kani::vec::any_vec::<u8, 64>();
let slice = vec.as_slice();
internet_checksum_intermediary::<4>(slice);
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 vec = kani::vec::any_vec::<u8, 64>();
let slice = vec.as_slice();
internet_checksum::<4>(0, slice);
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);
}
50 changes: 27 additions & 23 deletions src/ethernet/verification.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,13 @@ const HEADROOM: usize = SLICE_LENGTH + 10;

#[kani::proof]
fn get_ethernet_proof() {
let mut vec = kani::vec::any_vec::<u8, SLICE_LENGTH>();
let slice = vec.as_mut_slice();
let headroom = kani::any();
kani::assume(headroom < HEADROOM);
let mut any_array: [u8; SLICE_LENGTH] = kani::any();
let any_slice_length = kani::any_where(|i| *i <= SLICE_LENGTH);
let any_slice = &mut any_array[..any_slice_length];

if let Ok(mut to_test) = DataBuffer::<_, Eth>::new(slice, headroom) {
let any_headroom = kani::any_where(|i| *i <= HEADROOM);

if let Ok(mut to_test) = DataBuffer::<_, Eth>::new(any_slice, any_headroom) {
let _ = to_test.ethernet_destination();
let _ = to_test.ethernet_source();
let _ = to_test.ethernet_ether_type();
Expand All @@ -24,39 +25,42 @@ fn get_ethernet_proof() {

#[kani::proof]
fn set_ethernet_destination_proof() {
let mut vec = kani::vec::any_vec::<u8, SLICE_LENGTH>();
let slice = vec.as_mut_slice();
let headroom = kani::any();
kani::assume(headroom < HEADROOM);
let mut any_array: [u8; SLICE_LENGTH] = kani::any();
let any_slice_length = kani::any_where(|i| *i <= SLICE_LENGTH);
let any_slice = &mut any_array[..any_slice_length];

let any_headroom = kani::any_where(|i| *i <= HEADROOM);

if let Ok(mut to_test) = DataBuffer::<_, Eth>::new(slice, headroom) {
if let Ok(mut to_test) = DataBuffer::<_, Eth>::new(any_slice, any_headroom) {
let _ = to_test.set_ethernet_destination(&kani::any());
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), headroom).unwrap();
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), any_headroom).unwrap();
}
}

#[kani::proof]
fn set_ethernet_source_proof() {
let mut vec = kani::vec::any_vec::<u8, SLICE_LENGTH>();
let slice = vec.as_mut_slice();
let headroom = kani::any();
kani::assume(headroom < HEADROOM);
let mut any_array: [u8; SLICE_LENGTH] = kani::any();
let any_slice_length = kani::any_where(|i| *i <= SLICE_LENGTH);
let any_slice = &mut any_array[..any_slice_length];

if let Ok(mut to_test) = DataBuffer::<_, Eth>::new(slice, headroom) {
let any_headroom = kani::any_where(|i| *i <= HEADROOM);

if let Ok(mut to_test) = DataBuffer::<_, Eth>::new(any_slice, any_headroom) {
let _ = to_test.set_ethernet_source(&kani::any());
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), headroom).unwrap();
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), any_headroom).unwrap();
}
}

#[kani::proof]
fn set_ethernet_ether_type_proof() {
let mut vec = kani::vec::any_vec::<u8, SLICE_LENGTH>();
let slice = vec.as_mut_slice();
let headroom = kani::any();
kani::assume(headroom < HEADROOM);
let mut any_array: [u8; SLICE_LENGTH] = kani::any();
let any_slice_length = kani::any_where(|i| *i <= SLICE_LENGTH);
let any_slice = &mut any_array[..any_slice_length];

let any_headroom = kani::any_where(|i| *i <= HEADROOM);

if let Ok(mut to_test) = DataBuffer::<_, Eth>::new(slice, headroom) {
if let Ok(mut to_test) = DataBuffer::<_, Eth>::new(any_slice, any_headroom) {
let _ = to_test.set_ethernet_ether_type(kani::any());
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), headroom).unwrap();
DataBuffer::<_, Eth>::new(to_test.buffer_into_inner(), any_headroom).unwrap();
}
}
Loading

0 comments on commit b80b788

Please sign in to comment.