The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Dear Michael,

Register is indeed the manifestation of a hook mechanism in Coq’s kernel which I called retroknowledge. This mechanism allows the kernel to know about definitions from the standard library. What happens then, is that in vm_compute or native_compute, the compilation detects these 31-bit integers and their operation and compiles them to an efficient representation (they’re machine integers, but truncated to 32 bits for compatibility and the low bit fixed to 1 for the GC). At typing time, though, these are Coq terms so there was no need to invent new logic. If you have numerical-computation heavy code using Int31 (or BigN or BigZ) will probably give you a pretty big improvement in performances (though we’ve had mixed results with rational computations). At the price of a non-trivial increase in the trusted base.

This is not a perfect scheme though, because integer literals are, in fact, pretty big Coq terms, and so can be slow to type-check (there has been applications where type-checking the integer litteral was dominating any other performance bottleneck; in the ring tactic it can even be slower to use BigN coefficients instead of N). So there has been another scheme in the work, where new logic and black-box constant to represent machine-integers. This has proven even faster, but the changes to the kernel are trickier. I haven’t been involved in this project and I don’t know its status.

​

On 28 June 2016 at 13:50, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

I found it. The “Register” declarations get stripped from the generated documentation:

 

Register digits as int31 bits in "coq_int31" by True.

Register int31 as int31 type in "coq_int31" by True.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Soegtrop, Michael
Sent: Tuesday, June 28, 2016 12:42 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?

 

Dear Coq Users,

 

the In31 library

 

https://coq.inria.fr/library/Coq.Numbers.Cyclic.Int31.Int31.html

 

states that the Int31 type comes with an “underlying mechanism for hardware-efficient computations”. I wonder what this means and how it works. The addition in Int31 seems to be implemented by conversion to Z, addition in Z and conversion back.

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928