The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hi,

On 03/24/2014 07:15 AM, Arnaud Spiwack wrote:
> Just to be clear on the reason that Coq's native integers are 31 bits.
>
> Obviously the integers Coq uses have to be machine independent, out of 
> concern for consistency. We chose 31-bit because they fit in a machine 
> word of every (reasonable?) machine (the runtime reserves the last bit 
> of every word to tell the garbage collector whether we are in the 
> presence of a pointer or not).

I think it is fair to say that having machine-independent integers is a 
design choice, more than a constraint. We could have written a Coq 
library where the size of integers is instantiated once and for all 
according to the architecture. Only proofs relying specifically on the 
value of this size, and the .vo files, would no longer be portable 
across architectures.

> Of course, it would be arguably better to have 63bit integers and 
> emulate them on the 32bit architecture. However, there is a trick to 
> Coq: since it must evaluate open terms, there is a representation of 
> variables in the bytecode values. The integer operation are nonsense 
> on variables*. As it happens, variables (and more generally terms with 
> a variable in head position) are represented as blocks (aka pointers), 
> and so we use the gc-bit to discrimate: if we see a pointer, the 
> operations are done inefficiently, if we see a simple value, we use 
> the efficient processor arithmetic. We would need to replace this 
> trick with a more complex one for bigger integers to be emulated on a 
> 32-bit architecture.

Indeed, and we can do something similar to OCaml's Int64 values, which 
are blocks with specific ("custom") tags.

> Currently there has been some effort in having a more efficient 
> implementation of native integers into Coq. As it is more complex, it 
> still hasn't been integrated, I don't actually know where this 
> prototype stands on the issue of integer size.

I have a very experimental prototype with 63-bits integers (for the 
regular evaluation machine of the kernel, as well as the VM and the 
native compiler), but with no emulation support for the VM on 32-bits 
architectures yet. I gave a talk on this work at the last Coq Workshop: 
http://www.maximedenes.fr/download/coq_primitives.pdf

The reason why this prototype has not been integrated in Coq's trunk yet 
is not so much an additional complexity, but rather the desire to take 
the opportunity to polish the associated libraries. Which is a time 
consuming task, but seems necessary given their current shape :)

Maxime.

> [*] in fact, native integers are compiled from actual Coq terms which 
> can have variables in them, not necessarily in head position. So there 
> is an extra case which we have to handle: that of a constructed term. 
> Fortunately, the constructed terms with non-nullary constructors are 
> also pointers, and the catch-all case for pointers handle them properly.
>
>
> On 24 March 2014 08:46, Guillaume Melquiond 
> <guillaume.melquiond AT inria.fr <mailto:guillaume.melquiond AT inria.fr>> 
> wrote:
>
>     On 24/03/2014 07:10, Moshe Tenenbaum wrote:
>
>         Gabriel and Enrico, thank you very much for your responses!
>         Good step
>         forward for me.
>
>         My next question regards if there is any possible way to go a bit
>         further with the code. FOr example, in the coq_interp.c code you
>         mention, on line 1300, there is an instruction that looks like
>         this:
>
>         Instruct (TAIL0INT31) {
>              int r = 0;
>                  uint32 x;
>                  print_instr("TAIL0INT31");
>              x = (((uint32) accu >> 1) | 0x80000000);
>                  if (!(x & 0xFFFF)) { x >>= 16; r += 16; }
>                  if (!(x & 0x00FF)) { x >>= 8;  r += 8; }
>                  if (!(x & 0x000F)) { x >>= 4;  r += 4; }
>                  if (!(x & 0x0003)) { x >>= 2;  r += 2; }
>                  if (!(x & 0x0001)) { x >>=1;   r += 1; }
>                  if (!(x & 0x0001)) {           r += 1; }
>                  accu = value_of_uint32(r);
>                  Next;
>                }
>
>         Can this be transformed using mnemonics like uint64 instead of
>         uint32?
>
>
>     Sure, you can declare x of static type uint64. But presumably, any
>     optimizing compiler is already doing this transformation behind
>     the scenes when it is beneficial for performances.
>
>     You can even go further with mnemonics and substitute all of this
>     code with __builtin_ctz(x) (assuming this construct is portable
>     enough) and let the compiler do its black magic. That said, I
>     doubt that it would bring any noticeable speed-up.
>
>     (By the way, I am noticing that the last test is pointless, since
>     it always evaluates to false.)
>
>
>         And can it be extended for TAIL0INT63 for proper memory
>         allocation?
>
>
>     No, it can't. Keep in mind that this is just the tiny C part of a
>     huge Coq development about 31-bit integers. If you change the
>     width of integers there, you will have to modify some Coq theories
>     in depth and deal with the fallout of breaking user formalizations.
>
>     I am not saying it is a bad idea. In fact, I whole-heartedly
>     support switching Coq native integer from 31 bits to 63 bits in
>     the long run. I am just saying that this is a much more massive
>     endeavor than the code might suggest.
>
>     Best regards,
>
>     Guillaume