The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Thu, 24 Mar 2011 11:07:51 +0800,
geng chen 
<chengeng4001 AT gmail.com>
 a écrit :

> Hi, everyone
> 
> Recently, I need to define some type like int32 in C and operate the
> each bits of the number. For example in C, we can define bit field:
> typedef struct {
>     int a1         : 1;
>     int a2            : 1;
>     int a3              : 1;
>     int a4            : 1;
>     int a5             : 1;
>     int a6               : 1;
>     int a7            : 1;
>     int a8              : 1;
>     int a9               : 1;
>     int a10           : 3;
>     int a11   : 20;
> }aa;
> We can operate these fields in int32 numbers.
> Can we do the same thing in Coq? Could any body give me some advise?

In fact, in coq, there is no integer type.
You can take a look at compcert and other projects to see how to
represent these types.

Basically, I mainly see two ways:
one is by comprehension:
 -> define all the integers (even after 2^32), for that you can take a
 look at BinPos in the standard library:
  Inductive positive: Set :=
  | xH: positive (* for 1 *)
  | xO: positive -> positive (* for λx·2×x *)
  | xI: positive -> positive (* for λx·2×x+1 *)
  .
 Notes:
 * it cannot represent the "0" value unless you use an option type
   (and then None codes for 0). It is just to ensure canonicity of the
   writing, replacing
   "xH: positive (* for 1 *)" by
   "xZ: positive (* for 0 *)" may lead to a more natural
   representation, but you will have to deal with the fact that
   "xO xZ", "xO (xO xZ)", … are equivalent to "xZ"
 * there is some syntactic suger:
   1%positive for xH,
   2%positive for xO xH
   and you can even omit it by a "Open positive_scope"
 * This type is isomorphic to "list bool"
 -> define a < predicate (it is already done in some of the standard
 library), then define int32 as {i: option positive | i<2^32}.
 That is basically what is done in compcert (but using Z instead of
 positive, allowing you to have signed values), if I am not wrong.

the other is using some kind of bitvector:
 * Record int32: Set :=
   { b0: bool;
     b1: bool;
     b2: bool;
     …
     b31: bool
   }.
   So, you will have direct access to any bit (unlike the previous
   suggestion, where you need to shift n times to get the nth bit),
   but you will have to define all your operations (+, -, *, /, …)
   Note that you have this alternative:
   Record nibble: Set :=
   { b0: bool;
     b1: bool;
     b2: bool;
     b3: bool
   }.
   Record octet: Set :=
   { n0: nibble;
     n1: nibble
   }.
   Record short: Set :=
   { o0: octet;
     o1: octet
   }.
   Record int32: Set :=
   { s0: short;
     s1: short
   }.
   to define your int32, then accessing the 7th bit of i is:
   i.(s0).(o0).(n1).(b2)
   So if you define:
   Inductive nibble_loc: Set := B0|B1|B2|B3.
   Record bit_location: Set :=
   { hi_short: bool;
     hi_octet: bool;
     hi_nibble: bool;
     bit_loc: nibble_loc
   }.
   then a bit range would be a pair of two bit locations.
   (I didn't go below nibble, since it is less common
    and I don't know the word for pair of bits, but of
    course you can go below!)

To sum up, I advise you to take a look on the compcert project,
they have a good set of operations on integers, sorry I don't send you
a link, but I can't find the online documentation of compcert (I was
pretty sure there was one, but I don't find it).

But if you want your own library, my second point can be considered.

http://compcert.inria.fr/index.html