@@ -14,31 +14,18 @@ where
1414 let start = data. partition_point ( |x| key_fn ( x) < * key) ;
1515 // At this point `start` either points at the first entry with equal or
1616 // greater key or is equal to `size` in case all elements have smaller keys
17+ // Invariant: start == size || key_fn(&data[start]) >= *key
1718 if start == size || key_fn ( & data[ start] ) != * key {
1819 return & [ ] ;
1920 } ;
21+ // Invariant: start < size && key_fn(&data[start]) == *key
2022
21- // Now search forward to find the *last* one.
22- let mut end = start;
23- let mut previous = start;
24- let mut step = 1 ;
25- loop {
26- end = end. saturating_add ( step) . min ( size) ;
27- if end == size || key_fn ( & data[ end] ) != * key {
28- break ;
29- }
30- previous = end;
31- step *= 2 ;
32- }
33- step = end - previous;
34- while step > 1 {
35- let half = step / 2 ;
36- let mid = end - half;
37- if key_fn ( & data[ mid] ) != * key {
38- end = mid;
39- }
40- step -= half;
41- }
23+ // Find the first entry with key > `key`. Skip `start` entries since
24+ // key_fn(&data[start]) == *key
25+ // Invariant: offset == size || key_fn(&data[offset]) >= *key
26+ let offset = start + 1 ;
27+ let end = data[ offset..] . partition_point ( |x| key_fn ( x) <= * key) + offset;
28+ // Invariant: end == size || key_fn(&data[end]) > *key
4229
4330 & data[ start..end]
4431}
0 commit comments