parallel_count.pvl

class ParCount {
	ensures |xs| == 0 ==> \result == 0;
	ensures |xs| == 1 ==> \result == head(xs);
	ensures |xs| > 1 ==> \result == head(xs) + intsum(tail(xs));
	//ensures head(xs) == 0 ==> \result == 0 + intsum(tail(xs));
	ensures (\forall int i; i >= 0 && i < |xs|; xs[i] == 0) ==> intsum(xs) == 0;
    ensures intsum(xs) == 0 ==> (\forall int i; i >= 0 && i < |xs|; xs[i] == 0);
	static pure int intsum(seq<int> xs) =
		0 < |xs| ? head(xs) + intsum(tail(xs)) : 0;

	ensures intsum(seq<int> { }) == 0;
	void lemma_intsum_zero() {
	}
	
	ensures intsum(seq<int> { x }) == x;
	void lemma_intsum_single(int x) {
		assert tail(seq<int> { x }) == seq<int> { };
		lemma_intsum_zero();
	}
	
	
	requires |xs| > 0;
	requires head(xs) == 0;
	ensures intsum(xs) == intsum(tail(xs));
	void lemma_intsum_zeroVal(seq<int> xs) {
		assert intsum(xs) == intsum(tail(xs));
	}

	ensures \result == 2; // 0 + 2 + 3 + 3 + 2 == 10;
	int intsumTest() {
		seq<int> values = seq<int>{0, 2};
		return intsum(values);
	}
	ensures |sequence| + 1 == |\result|;
	static pure seq<int> prependToSeq(int value, seq<int> sequence) =
		seq<int>{value} + sequence;

	requires i >= 0 && i <= |sequence|;
	ensures |\result| == |sequence| - i;
	ensures |\result| == 0 ==> \result == seq<int>{};
	//ensures |\result| == 1 ==> \result == seq<int>{sequence[|sequence| - 1]};
	//ensures |\result| == 2 ==> \result == seq<int>{sequence[|sequence| - 2], sequence[|sequence| - 1]};
	ensures (\forall int j; j >= 0 && j < |\result|; \result[j] == sequence[j + i]);
	static pure seq<int> getRightSubSeq(seq<int> sequence, int i) =
		i < |sequence| ? seq<int>{sequence[i]} + getRightSubSeq(sequence, i + 1) : seq<int>{};

	requires loopIndex == intsum(sequence);
	requires incrementIndex >= 0 && incrementIndex < |sequence|;
	requires seqIterator >= 0 && seqIterator <= |sequence|;
	ensures seqIterator == |sequence| ==> |\result| == 0;
	ensures |\result| == |sequence| - seqIterator;
	ensures seqIterator == 0 ==> |sequence| == |\result|;
	//ensures \result[incrementIndex] == sequence[incrementIndex] + 1;
	//ensures (\forall int i; i >= 0 && i < |\result|; i == incrementIndex ? \result[i] == sequence[i] + 1 : \result[i] == sequence[i]);
	ensures seqIterator > incrementIndex ==> (\forall int i; i >= 0 && i < |\result| ; \result[i] == sequence[i+seqIterator]);
	ensures seqIterator <= incrementIndex ==> (\forall int i; i >= 0 && i < |\result| && i != incrementIndex-seqIterator; \result[i] == sequence[i+seqIterator]);
	ensures seqIterator <= incrementIndex  ==> (\result[incrementIndex-seqIterator] == (sequence[incrementIndex] + 1));

	ensures seqIterator == |sequence| ==> intsum(\result) == 0;
	//ensures seqIterator > incrementIndex ==> intsum(\result) == intsum(sequence[seqIterator..]);
	//ensures seqIterator == 0 && |\result| > 0 ==> intsum(sequence) + 1 == intsum(\result);
	static pure seq<int> incrementInnerSequence(seq<int> sequence, int seqIterator, int incrementIndex, int loopIndex) =
		seqIterator < |sequence| ? (seqIterator == incrementIndex ? 
			prependToSeq(sequence[seqIterator] + 1, incrementInnerSequence(sequence, seqIterator + 1, incrementIndex, loopIndex)) : 
			prependToSeq(sequence[seqIterator]    , incrementInnerSequence(sequence, seqIterator + 1, incrementIndex, loopIndex))) :
			seq<int>{};
/*
	static pure seq<seq<int>> incrementOuterSequence(seq<seq<int>> sequences, int seqSeqIterator, int seqIterator, int incrementIndex, int loopIndex) =
		seqSeqIterator < |sequences| ? (seqSeqIterator == seqIterator ?
			seq<seq<int>>{incrementInnerSequence()} + incrementOuterSequence(sequences, seqSeqIterator + 1, seqIterator, incrementIndex, loopIndex) :
			seq<seq<int>>{sequences[seqSeqIterator]} + incrementOuterSequence(sequences, seqSeqIterator + 1, seqIterator, incrementIndex, loopIndex)) :
			seq<seq<int>>{};
*/
	//ghost variables
	given seq<seq<int>> tempCountsGhost;
	//function invariants
	context_everywhere input != null && output != null && tempCounts != null;
	context_everywhere partitionSize >= 0 && tCount >= 0 && radix > 1;
	context_everywhere tCount >= radix;
	context_everywhere partitionSize * tCount == input.length;
	context_everywhere radix == output.length;
	context_everywhere tempCounts.length == tCount;
	context_everywhere |tempCountsGhost| == tempCounts.length;
	context_everywhere (\forall int i; i >= 0 && i < tempCounts.length; tempCounts[i].length == radix);
	context_everywhere (\forall int i; i >= 0 && i < tempCounts.length; tempCounts[i].length == |tempCountsGhost[i]|);
	context_everywhere output.length == radix;
	//permission specifications
	context (\forall* int i; i >= 0 && i < input.length; Perm(input[i], read));
	context (\forall* int i; i >= 0 && i < output.length; Perm(output[i], write));
	context (\forall* int i; i >= 0 && i < tCount;
		(\forall* int j; j >= 0 && j < radix; Perm(tempCounts[i][j], write)));

	//pre conditions
	requires (\forall int i; i >= 0 && i < input.length; input[i] >= 0 && input[i] < radix);
	requires (\forall int i; i >= 0 && i < tempCounts.length; 
		(\forall int j; j >= 0 && j < tempCounts[i].length; tempCounts[i][j] == 0));
	//functional correctness of count sum property
	requires (\forall int i; i >= 0 && i < |tempCountsGhost|; 
		(\forall int j; j >= 0 && j < |tempCountsGhost[i]|; tempCounts[i][j] == tempCountsGhost[i][j]));
	void parCount(int radix, int[] input, int[] output, int partitionSize, int tCount, int[][] tempCounts) {



		par count (int tid = 0..tCount)
			//permission specifications
			context (\forall* int i; i >= 0 && i < radix; Perm(tempCounts[tid][i], write));
			requires (\forall* int i; i >= (partitionSize * tid) && i < (partitionSize * (tid + 1)); Perm(input[i], read));
			//pre-conditions
			requires (\forall  int i; i >= (partitionSize * tid) && i < (partitionSize * (tid + 1)); input[i] >= 0 && input[i] < radix);
			//functional correctness of count sum property
			requires (\forall int i; i >= 0 && i < tempCounts[tid].length; tempCounts[tid][i] == 0); 
			requires (\forall int i; i >= 0 && i < tempCounts[tid].length; tempCounts[tid][i] == tempCountsGhost[tid][i]);
			{




			assert (\forall int i; i >= 0 && i < |tempCountsGhost[tid]|; tempCountsGhost[tid][i] == 0);
			assert intsum(tempCountsGhost[tid]) == 0;



			//permission invariants
			loop_invariant (\forall* int i; i >= 0 && i < radix; Perm(tempCounts[tid][i], write));
			loop_invariant (\forall* int i; i >= (partitionSize * tid) && i < (partitionSize * (tid + 1)); Perm(input[i], read));
			//helper invariants
			loop_invariant 0 <= i && i <= partitionSize;
			loop_invariant (\forall  int i; i >= (partitionSize * tid) && i < (partitionSize * (tid + 1)); input[i] >= 0 && input[i] < radix);
			//functional correctness of count sum property
			//loop_invariant intsum(tempCountsGhost[tid]) == i;
			loop_invariant (\forall int i; i >= 0 && i < tempCounts[tid].length; tempCounts[tid][i] == tempCountsGhost[tid][i]);
			for (int i = 0; i < partitionSize; i++) {
				int index = (tid * partitionSize) + i;
				int number = input[index];

				tempCounts[tid][number] = tempCounts[tid][number] + 1;

				int newValue = tempCountsGhost[tid][number] + 1;
				seq<int> newGhostCount = tempCountsGhost[tid][number -> newValue];
				tempCountsGhost = tempCountsGhost[tid -> newGhostCount];
				assert (\forall int i; i >= 0 && i < tempCounts[tid].length; tempCounts[tid][i] == tempCountsGhost[tid][i]);
				//assert intsum(tempCountsGhost[tid]) == i + 1;
				//assert false;
			}
			
			barrier(count) {
				//permissions specifications
				requires (\forall* int i; i >= 0 && i < radix; Perm(tempCounts[tid][i], write));
				requires (\forall* int i; i >= (partitionSize * tid) && i < (partitionSize * (tid + 1)); Perm(input[i], read));
				requires (\forall  int i; i >= (partitionSize * tid) && i < (partitionSize * (tid + 1)); input[i] >= 0 && input[i] < radix);

				ensures tid <= radix ==> (\forall* int i; i >= 0 && i < tCount; Perm(tempCounts[i][tid], write));
				ensures tid <= radix ==> Perm(output[tid], write);
				//functional correctness of count sum property
				//ensures (\forall int i; i >= 0 && i < tCount; intsum(valsMethod(1, extractArray(tempCounts, i), 0)) == partitionSize);
			}
			
			if (tid <= radix) {
				//permission invariant
				loop_invariant tid <= radix ==> (\forall* int i; i >= 0 && i < tCount; Perm(tempCounts[i][tid], write));
				loop_invariant tid <= radix ==> Perm(output[tid], write);
				//helper invariants
				loop_invariant tid >= 0 && tid <= radix;
				loop_invariant i >= -1 && i < tCount;
				//functional correctness of count sum property
				for (int i = tCount - 1; i >= 0; i--) {
					output[tid] = output[tid] + tempCounts[i][tid];
				}
			}
			barrier(count) {
				requires tid <= radix ==> (\forall* int i; i >= 0 && i < tCount; Perm(tempCounts[i][tid], write));
				requires tid <= radix ==> Perm(output[tid], write);

				ensures (\forall* int i; i >= 0 && i < radix; Perm(tempCounts[tid][i], write));
			}
		}
	}
}