I want to prove the correctness of some of my programs but I don't know where to start. Let's say I have the following program, how can I prove its correctness or lack there of. How can I go from the source below and plug them into a theorem prover. Coq or ACL2 or pretty much anything.
The code below just counts the bytes that it reads from the standard input. It has 2 versions, one does a byte by byte count, the other reads them by unsigned integer size chunks when possible. I know it's not portable or pretty, it's just an example that could get me started. With some help.
The code works and I know it's correct and I know how to write unit tests for it but I don't know how to prove anything about it.
#include <stdio.h>
#include <unistd.h>
#include <stdlib.h>
unsigned count_bytes1(unsigned char * bytes, unsigned len) {
unsigned count=0;
unsigned i;
for (i=0;i<len;i++) {
count+=bytes[i];
}
return count;
}
unsigned count_word(unsigned word) {
unsigned tmp = word;
if (sizeof(unsigned)==4) {
tmp = (0x00FF00FFU&tmp) + (( (0xFF00FF00U)&tmp)>>8);
tmp = (0x0000FFFFU&tmp) + (( (0xFFFF0000U)&tmp)>>16);
return tmp;
}
if (sizeof(unsigned)==8) {
tmp = (0x00FF00FF00FF00FFU&tmp) + (( (0xFF00FF00FF00FF00U)&tmp)>>8);
tmp = (0x0000FFFF0000FFFFU&tmp) + (( (0xFFFF0000FFFF0000U)&tmp)>>16);
tmp = (0x00000000FFFFFFFFU&tmp) + (( (0xFFFFFFFF00000000U)&tmp)>>32);
return tmp;
}
return tmp;
}
unsigned count_bytes2(unsigned char * bytes, unsigned len) {
unsigned count=0;
unsigned i;
for (i=0;i<len;) {
if ((unsigned long long)(bytes+i) % sizeof(unsigned) ==0) {
unsigned * words = (unsigned *) (bytes + i);
while (len-i >= sizeof(unsigned)) {
count += count_word (*words);
words++;
i+=sizeof(unsigned);
}
}
if (i<len) {
count+=bytes[i];
i++;
}
}
return count;
}
int main () {
unsigned char * bytes;
unsigned len=8192;
bytes=(unsigned char *)malloc(len);
len = read (0,bytes,len);
printf ("%u %u\n",count_bytes1(bytes,len),count_bytes2(bytes,len));
return 0;
}
First, decide what it is you want to prove for your function. For instance, write a contract for your function, using the ACSL specification language:
/*@ ensures \result >= x && \result >= y;
ensures \result == x || \result == y;
*/
int max (int x, int y);
Then, you may prove that your implementation satisfies the specification, for instance with Frama-C's WP plug-in.
The WP plug-in will generate proof obligations, the verification of which will ensure that the implementation is correct with respect to the specification. You can prove these in Coq 8.4+ if it amuses you (but almost nobody who actually does this does not first apply available, fully automatic SMT provers such as Alt-Ergo).
PS: it appears that you are trying to prove that one C function is equivalent to another, that is, to use a simple C function as specification for an optimized one. Proving the equivalence of one with respect to the other is the approach followed in this article:
José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, and Bárbara Vieira. Verifying cryptographic software correctness with respect to reference implementations. In FMICS’09, volume 5825 of LNCS, pages 37–52, 2009.