diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-05 04:13:33 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-05 04:13:33 +0000 |
| commit | 0f5087bea45be49e105727d6cee4194598474fee (patch) | |
| tree | 6155d21f87a98b34ad232504d1124657ec4ed359 /lib/Integers.v | |
| parent | 1b21b6d72a4cdeb07ad646e7573983faaae47399 (diff) | |
Back from Oregon commit.
powerpc/*: better compilation of some comparisons; revised asmgenproof1.
common/*: added Mem.storebytes; used to give semantics to memcpy builtin.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1679 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 30f692a..6e7a6cb 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -167,6 +167,11 @@ Definition divu (x y: int) : int := Definition modu (x y: int) : int := repr (Zmod (unsigned x) (unsigned y)). +Definition add_carry (x y cin: int): int := + if zlt (unsigned x + unsigned y + unsigned cin) modulus + then zero + else one. + (** For bitwise operations, we need to convert between Coq integers [Z] and their bit-level representations. Bit-level representations are represented as characteristic functions, that is, functions [f] @@ -746,6 +751,11 @@ Proof. rewrite Zplus_0_r. apply repr_unsigned. Qed. +Theorem add_zero_l: forall x, add zero x = x. +Proof. + intros. rewrite add_commut. apply add_zero. +Qed. + Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z). Proof. intros; unfold add. |