The Coq mailing list

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

It used n=8 indeed. To elaborate (though Laurent could speak of it much better than I could), it was represented as a 256-constructor enumerated types. Since in the VM (and now native compilation) constant constructors are represented as unboxed words, this was fairly efficient (though on a 32-bit machine roughly a fourth of the real estate in each word was wasted). In fact, combined with using a tree representation rather than a list representation, this blew binary numbers (like Coq’s N and Z) out of the water. Because of how Coq’s pattern-matching, the size of the file defining arithmetic n the digits (which was mercifully generated) was roughly quadratic in 2^n. I had made back of the envelope calculations and estimated that using 2^16 constructors would lead to a file over 1GB long. At any rate switching to 2^31 digits (for maximal utilisation of real estate on 32-bit machines) lead to a very significant speed-up (though empirical evidences from Benjamin Grégoire suggest that it may not be the best trade-off, and using 64-bit boxed integers may work better). My most recent thoughts on the subject (though admittedly not fresh) can be found in the third chapter of my PhD dissertation [ http://assert-false.net/arnaud/papers/thesis.spiwack.pdf#chapter.3 ].

For a safe mode, I can see two ways to go. The first one is to use the external checker shipped with Coq which does not know of native integers (nor of the VM, for that matter), unfortunately, it is very likely to turn almost-instantaneous computations to computations which will not end in my lifetime (since native integers have such horrible computation property when they are not compiled specially). Another approach would be to parametrise your code to be able to switch integer implementation (one can imagine a module which, depending on options of the build system imports one of two number implementations). To facilitate that, it may be useful if the use of native integer was flagged by Print Assumptions, though it isn’t currently.

​

​

On 29 June 2016 at 20:29, Laurent Thery <Laurent.Thery AT inria.fr> wrote:

On 06/29/2016 11:45 AM, Soegtrop, Michael wrote:

Dear Arnaud,



thanks a lot for the detailed explanation – the “Register” process
doesn’t seem to be documented in the reference manual, so this is very
welcome.



I would say the trust base increase is not that much of a problem, as
long as this can be switched off easily. I don’t see how this would be
done in the current implementation of Int32 (other than copying the
library and removing the register keyword). I would use such features
mostly for interactive development and use the plain Coq implementation
in overnight check runs, where speed doesn’t matter that much.

Hi,

The first version of the Big library as described in

A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. IJCAR 2006.

was using what you propose. A type with 2^n constructions such that the basic operations where encoded by direct pattern matching.
My memory was the biggest n Coq could handle was n = 8.
Then thanks to Arnaud we use the native int31 but I agree with you
it would be good to give the possibility to switch to a "safe" mode.

-
Laurent






We were using

Btw.: has it been tried to use e.g. hex digit representations in Coq?
This thesis analyses the speed up of multi-bit digit arithmetic in HOL:



FORMAL COMPUTATIONS AND METHODS by Alexey Solovyev, Pittsburgh, 2007



http://d-scholarship.pitt.edu/16721/7/SolovyevThesis_(v._1.02).pdf



For 5 decimal digit numbers the speed up is about 2.5, from 10 decimal
digits on one gets a speed increase of about 4 times for 4 bit digits.



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