how to prove the correctness of a c program with coq

Question

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;
}

Answer 1

1. Know what you are proving: specification

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);

2. Verification

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.