-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathunique-contract.txt
143 lines (143 loc) · 11.4 KB
/
unique-contract.txt
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
de.wiesler.BucketPointers[de.wiesler.BucketPointers::alignedBoundariesKeepEnoughSpace(int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::BucketPointers([I,int,int,[I)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::bucketSize(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::bucketStart(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::countElement([I,int,int,[I,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::decrement_read(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::disjointBucketsAreaLemma([I,int,int,int,int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::disjointBucketsLemma(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::elementsToReadCountClassEq(de.wiesler.Classifier,[I,int,int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::elementsToReadCountClassEqSplitBucket(de.wiesler.Classifier,[I,int,int,int,int,boolean)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::elementsToReadCountElement([I,int,int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::elementsToReadCountElementSplitBucket([I,int,int,int,int,boolean)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::elementsToReadOfBucketBlockClassified(de.wiesler.Classifier,[I,int,int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::elementsToReadOfBucketCountClassEq(de.wiesler.Classifier,[I,int,int,int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::elementsToReadOfBucketCountElement([I,int,int,int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::hasRemainingRead(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::increment_write(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::initialReadAreasBlockClassified(de.wiesler.Classifier,[I,int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::initialReadAreasCount([I,int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::initialReadAreasCountBucketElements(de.wiesler.Classifier,[I,int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::initialReadAreasCountBucketElementsLemma(de.wiesler.Classifier,[I,int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::initialReadAreasCountLemma([I,int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::isAtInitialBucketState(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::isAtInitialState()]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::isValidBucketPointer(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::lastReadOf(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::nextWriteOf(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::overflowBucketUniqueLemma(int,int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::readIsMaximal(int,int,int,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::remainingWriteCountOfBucket(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::toReadCountOfBucket(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::write(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::writtenCountOfBucket(int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::writtenElementsCountElement([I,int,int,[I,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::writtenElementsCountElementSplitBucket([I,int,int,[I,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::writtenElementsOfBucketClassified(de.wiesler.Classifier,[I,int,int,[I,int)]
de.wiesler.BucketPointers[de.wiesler.BucketPointers::writtenElementsOfBucketCountElement([I,int,int,[I,int,int)]
de.wiesler.Buffers[de.wiesler.Buffers::align_to_next_block(int)]
de.wiesler.Buffers[de.wiesler.Buffers::blockAligned(int)]
de.wiesler.Buffers[de.wiesler.Buffers::bufferElement(int,int)]
de.wiesler.Buffers[de.wiesler.Buffers::bufferLen(int)]
de.wiesler.Buffers[de.wiesler.Buffers::Buffers([I,[I,int)]
de.wiesler.Buffers[de.wiesler.Buffers::bufferSizeForBucketLen(int)]
de.wiesler.Buffers[de.wiesler.Buffers::count()]
de.wiesler.Buffers[de.wiesler.Buffers::countElement(int)]
de.wiesler.Buffers[de.wiesler.Buffers::countElementInBucket(int,int)]
de.wiesler.Buffers[de.wiesler.Buffers::distribute(int,[I,int,int,int,int)]
de.wiesler.Buffers[de.wiesler.Buffers::flush(int,[I,int,int)]
de.wiesler.Buffers[de.wiesler.Buffers::isBlockAligned(int)]
de.wiesler.Buffers[de.wiesler.Buffers::isBlockAlignedAdd(int,int)]
de.wiesler.Buffers[de.wiesler.Buffers::isBlockAlignedSub(int,int)]
de.wiesler.Buffers[de.wiesler.Buffers::isClassifiedWith(de.wiesler.Classifier)]
de.wiesler.Buffers[de.wiesler.Buffers::isEmpty()]
de.wiesler.Buffers[de.wiesler.Buffers::len(int)]
de.wiesler.Buffers[de.wiesler.Buffers::push(int,int)]
de.wiesler.Classifier[de.wiesler.Classifier::allElementsCounted([I,int,int,[I)]
de.wiesler.Classifier[de.wiesler.Classifier::calculate_bucket_starts([I,int,int,int,[I,de.wiesler.Buffers)]
de.wiesler.Classifier[de.wiesler.Classifier::Classifier([I,[I,int,boolean)]
de.wiesler.Classifier[de.wiesler.Classifier::classify(int)]
de.wiesler.Classifier[de.wiesler.Classifier::classify_all([I,int,int,[I)]
de.wiesler.Classifier[de.wiesler.Classifier::classify_locally([I,int,int,[I,de.wiesler.Buffers)]
de.wiesler.Classifier[de.wiesler.Classifier::classify_locally_batched([I,int,int,[I,de.wiesler.Buffers)]
de.wiesler.Classifier[de.wiesler.Classifier::classOf(int)]
de.wiesler.Classifier[de.wiesler.Classifier::classOfClassifiedBlockFromFirst([I,int,int,int)]
de.wiesler.Classifier[de.wiesler.Classifier::classOfFirstSplitters()]
de.wiesler.Classifier[de.wiesler.Classifier::classOfTrans()]
de.wiesler.Classifier[de.wiesler.Classifier::countClassOfSliceEq([I,int,int,int)]
de.wiesler.Classifier[de.wiesler.Classifier::countClassOfSliceEqLemma([I,int,int,int)]
de.wiesler.Classifier[de.wiesler.Classifier::countElement([I,int,int,int,int,de.wiesler.Buffers,int)]
de.wiesler.Classifier[de.wiesler.Classifier::equal_buckets()]
de.wiesler.Classifier[de.wiesler.Classifier::finish_batch([I,[I,int,int,int,int,[I,de.wiesler.Buffers)]
de.wiesler.Classifier[de.wiesler.Classifier::from_sorted_samples([I,[I,int,int)]
de.wiesler.Classifier[de.wiesler.Classifier::isClassifiedAs(int,int)]
de.wiesler.Classifier[de.wiesler.Classifier::isClassifiedBlock([I,int,int)]
de.wiesler.Classifier[de.wiesler.Classifier::isClassifiedBlocksRange([I,int,int)]
de.wiesler.Classifier[de.wiesler.Classifier::isClassifiedBlocksRangeSplit([I,int,int,int)]
de.wiesler.Classifier[de.wiesler.Classifier::isClassifiedUntil([I,int,int,int,[I,de.wiesler.Buffers)]
de.wiesler.Classifier[de.wiesler.Classifier::isClassOfSlice([I,int,int,int)]
de.wiesler.Classifier[de.wiesler.Classifier::isClassOfSliceCopy([I,int,[I,int,int,int)]
de.wiesler.Classifier[de.wiesler.Classifier::isClassOfSliceSplit([I,int,int,int,int)]
de.wiesler.Classifier[de.wiesler.Classifier::isValidBufferLen(int,int)]
de.wiesler.Classifier[de.wiesler.Classifier::num_buckets()]
de.wiesler.Cleanup[de.wiesler.Cleanup::cleanedUpSlice([I,int,int,int,int,de.wiesler.Classifier,int)]
de.wiesler.Cleanup[de.wiesler.Cleanup::cleanup([I,int,int,de.wiesler.Buffers,[I,de.wiesler.BucketPointers,de.wiesler.Classifier,[I)]
de.wiesler.Constants[de.wiesler.Constants::isLog2Of(int,int)]
de.wiesler.Constants[de.wiesler.Constants::log2(int)]
de.wiesler.Functions[de.wiesler.Functions::bucketStartsOrdering([I,int,int)]
de.wiesler.Functions[de.wiesler.Functions::copy_nonoverlapping([I,int,[I,int,int)]
de.wiesler.Functions[de.wiesler.Functions::copy_unique([I,int,int,int,int,[I)]
de.wiesler.Functions[de.wiesler.Functions::countElement([I,int,int,int)]
de.wiesler.Functions[de.wiesler.Functions::countElementSplit([I,int,int,int)]
de.wiesler.Functions[de.wiesler.Functions::fill([I,int,int,int)]
de.wiesler.Functions[de.wiesler.Functions::isSortedSeqTransitive(\seq)]
de.wiesler.Functions[de.wiesler.Functions::isSortedSeqTransitiveFromSlice([I,int,int)]
de.wiesler.Functions[de.wiesler.Functions::isSortedSlice([I,int,int)]
de.wiesler.Functions[de.wiesler.Functions::isSortedSliceTransitive([I,int,int)]
de.wiesler.Functions[de.wiesler.Functions::isValidBucketStarts([I,int)]
de.wiesler.Functions[de.wiesler.Functions::max(int,int)]
de.wiesler.Functions[de.wiesler.Functions::min(int,int)]
de.wiesler.Functions[de.wiesler.Functions::select_n([I,int,int,int)]
de.wiesler.Increment[de.wiesler.Increment::Increment(boolean,int)]
de.wiesler.Partition[de.wiesler.Partition::allBucketsClassified([I,int,int,de.wiesler.Classifier,[I)]
de.wiesler.Partition[de.wiesler.Partition::bucketCountsToTotalCount([I,int,int,[I,int)]
de.wiesler.Partition[de.wiesler.Partition::partition([I,int,int,[I,de.wiesler.Classifier,de.wiesler.Storage)]
de.wiesler.PartitionResult[de.wiesler.PartitionResult::PartitionResult(int,boolean)]
de.wiesler.Permute[de.wiesler.Permute::countBucketElementsEverywhere([I,int,int,int,de.wiesler.BucketPointers,de.wiesler.Classifier)]
de.wiesler.Permute[de.wiesler.Permute::permute([I,int,int,de.wiesler.Classifier,de.wiesler.BucketPointers,[I,[I,[I)]
de.wiesler.Permute[de.wiesler.Permute::place_block(int,[I,int,int,de.wiesler.Classifier,de.wiesler.BucketPointers,[I,[I,[I)]
de.wiesler.Permute[de.wiesler.Permute::swap_block(int,[I,int,int,de.wiesler.Classifier,de.wiesler.BucketPointers,[I,[I,[I)]
de.wiesler.SampleParameters[de.wiesler.SampleParameters::isValidForLen(int)]
de.wiesler.SampleParameters[de.wiesler.SampleParameters::log_buckets(int)]
de.wiesler.SampleParameters[de.wiesler.SampleParameters::oversampling_factor(int)]
de.wiesler.SampleParameters[de.wiesler.SampleParameters::SampleParameters(int)]
de.wiesler.Sorter[de.wiesler.Sorter::allBucketsInRangeSorted([I,int,int,[I,int,int,int)]
de.wiesler.Sorter[de.wiesler.Sorter::allBucketsPartitioned([I,int,int,[I,int)]
de.wiesler.Sorter[de.wiesler.Sorter::allBucketsPartitionedLemma(de.wiesler.Classifier,[I,int,int,[I)]
de.wiesler.Sorter[de.wiesler.Sorter::base_case_sort([I,int,int)]
de.wiesler.Sorter[de.wiesler.Sorter::bucketIndexFromOffset([I,int,int)]
de.wiesler.Sorter[de.wiesler.Sorter::equalityBucketsInRange([I,int,int,[I,int,int,int)]
de.wiesler.Sorter[de.wiesler.Sorter::equalityBucketsLemma(de.wiesler.Classifier,[I,int,int,[I)]
de.wiesler.Sorter[de.wiesler.Sorter::fallback_sort([I,int,int)]
de.wiesler.Sorter[de.wiesler.Sorter::isBucketPartitioned([I,int,int,int,int)]
de.wiesler.Sorter[de.wiesler.Sorter::isEqualityBucket([I,int,int)]
de.wiesler.Sorter[de.wiesler.Sorter::nonEmptyBucketsLemma(de.wiesler.Classifier,[I,int,int,[I)]
de.wiesler.Sorter[de.wiesler.Sorter::notAllValuesInOneBucket([I,int,int)]
de.wiesler.Sorter[de.wiesler.Sorter::notAllValuesInOneBucketLemma([I,int,int)]
de.wiesler.Sorter[de.wiesler.Sorter::partition([I,int,int,[I,de.wiesler.Storage)]
de.wiesler.Sorter[de.wiesler.Sorter::sample([I,int,int,de.wiesler.Storage)]
de.wiesler.Sorter[de.wiesler.Sorter::sample_sort([I,int,int,de.wiesler.Storage)]
de.wiesler.Sorter[de.wiesler.Sorter::sample_sort_recurse_on([I,int,int,de.wiesler.Storage,[I,int,boolean,int)]
de.wiesler.Sorter[de.wiesler.Sorter::smallBucketIsSorted([I,int,int,int,int)]
de.wiesler.Sorter[de.wiesler.Sorter::smallBucketsInRangeSorted([I,int,int,[I,int,int,int)]
de.wiesler.Sorter[de.wiesler.Sorter::sort([I)]
de.wiesler.Sorter[de.wiesler.Sorter::sort([I,int,int,de.wiesler.Storage)]
de.wiesler.Sorter[de.wiesler.Sorter::sortednessFromPartitionSorted([I,int,int,[I,int)]
de.wiesler.Storage[de.wiesler.Storage::createArray(int)]
de.wiesler.Storage[de.wiesler.Storage::Storage()]
de.wiesler.Tree[de.wiesler.Tree::build(int,[I,int,int)]
de.wiesler.Tree[de.wiesler.Tree::classify(int)]
de.wiesler.Tree[de.wiesler.Tree::classify_all([I,int,int,[I)]
de.wiesler.Tree[de.wiesler.Tree::classOfFirstSplitters()]
de.wiesler.Tree[de.wiesler.Tree::isClassifiedAs(int,int)]
de.wiesler.Tree[de.wiesler.Tree::Tree([I,[I,int)]