Model and Prove Unsigned Integer Operation Wrapping Behavior in Coq

Question

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.

Answer 1

Here's one way to do the actual proof. The value of $n$ doesn't really matter, of course, but I just used what you had in your question.

Require Export ZArith Utf8 ssrbool ssrfun ssreflect.

Open Scope Z_scope.

Definition n := 2^32.

Goal ∀ a b : Z, 0 <= a < n → 0 <= b < n → (a + b) mod n < a ↔ a + b >= n.
Proof.
  split => [/[swap] | ] ?; last rewrite -(Z_mod_plus _ (-1));
           rewrite ? Zmod_small; intuition.
Qed.

The lemmas used above are from the Coq Standard Library.

The above version of the proof is compact, but hard to follow for beginners. Here is a more beginner-friendly proof:

Require Export ZArith Utf8 ssrbool ssrfun ssreflect.

Open Scope Z_scope.

Definition n := 2^32.

Goal ∀ a b : Z, 0 <= a < n → 0 <= b < n → (a + b) mod n < a ↔ a + b >= n.
Proof.
  split.
  - move=> H1 H2.
    contradict H1.
    rewrite Zmod_small; intuition.
  - rewrite -(Z_mod_plus (a + b) (-1) n); intuition.
    rewrite Zmod_small; intuition.
Qed.

Answer 2

One good source of inspiration for bounded integer is the CompCert C compiler¹. In particular, you may take a look at the Integer.v² file.

As you can see there, bounded integers (say, int32) are represented as a pair of an integer, and a proof that this integer is within bounds. Formally:

Record int: Type := mkint { intval: Z; intrange: -1 < intval < modulus }.

From there, you may define the various overflowing semantics depending on your language and operations of interest: wrapping, undefined behaviors, and so on...

¹ https://compcert.org/

² https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v

Answer 3

The Coq standard library includes two primitive integer libraries: Uint63 and Sint63 for unsigned and signed 63 bit integers respectively. They behave cyclically:

From Coq Require Import Uint63.
Open Scope uint63_scope.

Eval compute in (max_int + 1).
(*     
     = 0
     : int
*)

You can implement your overflow check as follows:

Definition add_overflow (a b : int) : bool :=
  if a + b <? a then
    true
  else
    false.

Of course, the above is needlessly verbose when the following does the same job:

Definition add_overflow' (a b : int) : bool := a + b <? a.

Then one could prove that this overflow check is correct. In order to state such a fact, we need to pick numbers that live outside the primitive integers, which we can add and check for overflow. For example:

From Coq Require Import ZArith Lia.
Open Scope Z_scope.


Lemma add_overflow_correct (a b : int) :
  add_overflow a b = true (* our function thinks a + b overflows *)
  <->
  to_Z max_int < to_Z a + to_Z b. (* a + b overflows *)
Admitted.