@@ -886,25 +886,56 @@ pub mod smallsort_verify {
886
886
887
887
// Run with these CLI args for now:
888
888
// function-contracts -Z mem-predicates --harness smallsort --no-default-checks --default-unwind 10
889
-
889
+
890
+ /*
891
+ Prove absence of undefined behavior of the following public functions.
892
+
893
+ <T as slice::sort::shared::smallsort::StableSmallSortTypeImpl>::small_sort
894
+ <T as slice::sort::shared::smallsort::UnstableSmallSortTypeImpl>::small_sort
895
+ <T as slice::sort::shared::smallsort::UnstableSmallSortFreezeTypeImpl>::small_sort
896
+ slice::sort::shared::smallsort::swap_if_less
897
+ slice::sort::shared::smallsort::insertion_sort_shift_left
898
+ slice::sort::shared::smallsort::sort4_stable
899
+ slice::sort::shared::smallsort::has_efficient_in_place_swap
900
+
901
+ Write contracts for the following public functions that show that they actually sort the slices.
902
+
903
+ <T as slice::sort::shared::smallsort::StableSmallSortTypeImpl>::small_sort
904
+ <T as slice::sort::shared::smallsort::UnstableSmallSortTypeImpl>::small_sort
905
+ <T as slice::sort::shared::smallsort::UnstableSmallSortFreezeTypeImpl>::small_sort
906
+
907
+ The memory safety and the contracts of the above listed functions must be verified for all
908
+ possible slices with arbitrary valid length.
909
+ */
890
910
#[ kani:: proof]
891
911
fn has_efficient_in_place_swap_proof ( ) {
892
912
has_efficient_in_place_swap :: < u8 > ( ) ;
893
913
}
894
914
895
- /*
915
+ // swap_if_less<T, F>(v_base: *mut T, a_pos: usize, b_pos: usize, is_less: &mut F)
896
916
#[ kani:: proof]
897
917
fn swap_if_less_proof ( ) {
898
-
918
+ let mut x: [ u8 ; SMALL_SORT_FALLBACK_THRESHOLD ] = kani:: any ( ) ;
919
+ let v_base = x. as_mut_ptr ( ) ;
920
+ let a_pos = kani:: any :: < usize > ( ) ;
921
+ let b_pos = kani:: any :: < usize > ( ) ;
922
+ kani:: assume ( a_pos < SMALL_SORT_FALLBACK_THRESHOLD ) ;
923
+ kani:: assume ( b_pos < SMALL_SORT_FALLBACK_THRESHOLD ) ;
924
+
925
+ swap_if_less
899
926
}
900
927
928
+ /*
929
+
930
+
901
931
#[kani::proof]
902
932
fn sort4_stable_proof() {
903
933
904
934
}
905
935
*/
906
936
907
937
#[ kani:: proof]
938
+ #[ kani:: should_panic]
908
939
fn insertion_sort_shift_left_proof ( ) {
909
940
let mut x: [ u8 ; SMALL_SORT_FALLBACK_THRESHOLD ] = kani:: any ( ) ;
910
941
let offset: usize = kani:: any ( ) ;
@@ -913,14 +944,6 @@ pub mod smallsort_verify {
913
944
insertion_sort_shift_left ( & mut x, offset, & mut |lhs, rhs| lhs < rhs) ;
914
945
}
915
946
916
- #[ kani:: proof]
917
- #[ kani:: should_panic]
918
- fn insertion_sort_shift_left_panics ( ) {
919
- let mut x: [ u8 ; SMALL_SORT_FALLBACK_THRESHOLD ] = kani:: any ( ) ;
920
- let offset: usize = kani:: any ( ) ;
921
- insertion_sort_shift_left ( & mut x, offset, & mut |lhs, rhs| lhs < rhs) ;
922
- }
923
-
924
947
#[ kani:: proof]
925
948
fn stable_small_sort_type_impl_proof ( ) {
926
949
// Small sort threshold is 16.
0 commit comments