1
$\begingroup$

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.

$\endgroup$

3 Answers 3

1
$\begingroup$

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.
$\endgroup$
5
  • $\begingroup$ Great answer. You seem pro at this. How have you learned these? I have been reading Software Foundations for a few weeks, but I don't think I've made much progress. $\endgroup$ Apr 8, 2023 at 10:45
  • 1
    $\begingroup$ I am a mathematician, not a programmer, so my interest lies in math proofs rather than software verification. I recommend Programs and Proofs by Ilya Sergey, and Mathematical Components by Mahboubi and Tassi; both books are linked from the MathComp docs at math-comp.github.io/documentation.html. MathComp is much better than bare Coq, as the MathComp system is more tailored towards math proofs, with a higher level of polish and user convenience. Having concrete things that you want to prove is essential for keeping up your motivation. As with everything else, practice is key. $\endgroup$
    – djao
    Apr 9, 2023 at 1:12
  • 1
    $\begingroup$ A new book, but one which looks very promising, is An Introduction to MathComp-Analysis by Reynald Affeldt, available at math.nagoya-u.ac.jp/~garrigue/lecture/2022_affeldt $\endgroup$
    – djao
    Apr 9, 2023 at 1:33
  • $\begingroup$ Thanks for the recommendation. I will check them out. I haven't heard about MathComp before. Is MathComp to Coq something like mathlib to Lean? $\endgroup$ Apr 9, 2023 at 7:33
  • 1
    $\begingroup$ As the name indicates, MathComp is a library of Mathematical Components, whereas mathlib in Lean is more like a library of mathematics. So yes they are similar but not quite the same thing. I view MathComp as more of a toolkit where they try to implement the most important constructions that you might need in your own proofs (e.g. groups, vector spaces, polynomials, etc.) whereas mathlib tries to prove all the theorems in math. $\endgroup$
    – djao
    Apr 10, 2023 at 14:32
2
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.