I'm learning Coq and trying to do something useful with it. For daily programming tasks, especially binary parsing, one of the things I must deal with is to check and handle integer arithmetic overflows. I want to model integer overflow/wrapping behavior in Coq and verify a specific method for detecting (or avoiding) overflow can work as expected.
For example, one method to check unsigned integer addition overflow is (extracted from here):
uint32_t a;
uint32_t b;
uint32_t result = a + b;
if (result < a) {
// overflow
} else {
// ok
}
To represent the same logic mathematically:
n = 2 ^ 32
forall. a b
0 <= a < n /\ 0 <= b < n,
we have
(a + b) mod n < a <-> a + b >= n
Then I'm stuck here. I'm not sure how to represent this in Coq. Neither do I know how to prove it. I'm not a professional mathematician. I guess it relates to modular arithmetic in mathematics and I should use some types and theorems in ZArith
. Googling about proving integer overflows in Coq doesn't yield very useful results for my specific problem.
I will be grateful if you can give me some hints.