coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] 64-bit integers

From: Xavier Leroy <Xavier.Leroy AT inria.fr>
To: coq-club AT inria.fr, Eddy Westbrook <westbrook AT galois.com>
Subject: Re: [Coq-Club] 64-bit integers
Date: Sat, 13 Jan 2018 17:09:31 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=xavier.leroy AT gmail.com; spf=Pass smtp.mailfrom=xavier.leroy AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f49.google.com
Ironport-phdr: 9a23:PCHeSxLa67BJmhLm7NmcpTZWNBhigK39O0sv0rFitYgeLvjxwZ3uMQTl6Ol3ixeRBMOHs6sC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffxhEiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QKsqUjq+8ahkVB7oiD8GNzEn9mHXltdwh79frB64uhBz35LYbISTOfFjfK3SYMkaSHJaXshMSSJBDIOyYYgBAeUPMulXrZXyqVQVoBuiBgShHv/jxiNGi3L026AxzuQvERvB3AwlB98BsW7brMv0NKgMS+C+0a/GwivZb/NR2Tb29Y/FfRE7rvGSXLJ/b9DRxVMpGQzblFWQrozkMiiU1uQLqWib7vBvWfihi249sgx8pCWkyMkrionMnI0Vy1bE+D14wIYzP924SVR0bcSqEJtKsSyRKoh4Qts6Tmxqtys20KAKtYC7cSQQy5kr2QTTZvODfoSQ4R/vSvydLSl2iX9nYr6yhQu+/VK9xuD4S8W51ktBoDBfndnWrH8N0gTe6siZRft5+UeswTOP2BrS6uFAOEw1m6/bJ4I4zr4+mZcetV7PHiDxmEXxg6+Wclsr9vK05OTgZ7Xqvp6cN4lqhQHiKqkjmMOyDf4lPgQQX2WX4+ex2KP58UD2RLhGlvg2nbPYsJDeK8QbvKm5AwpN34cs8Rm/ETam38oCnXUdKFJKZgiHj4/pOlzVL/D4CO2wg1WokDtx2//GObjhDo3XLnffiLfhYap960lExQUvytBf/otYBa0FIPLuQUD8r8fYDx88Mwys2enrEtR91oUEWWKOGKCVKq3SsUXbrt4oduKLfcoevCv3A/kj/f/ny3Ej3RcwcaW4laQac2yyBPNhIA3Nfnf3nt0bFmAJlgU3SOvrkxuJVjsFNFioWKdp1jglCY+8RaPOXIe8yOix1Tm6E4cQQm1cDUGkEHHydozCVe1aO3HaGdNojjFRDevpcIQmzxz78Vaik+M2fNqRwTURsNfY7PYw4uTSkR8o8jktVpaS1miMSyd/mWZaHmZqjpA6mlR0zxK46YY9m+ZRTIUB6PZAUwN8PpnZnbQjVoLCHznZd9LMc26IB9WrBTZrE4A0yt4KJll4Q5Cs0kGF0C2tDLsY0beMAc5s/w==

On 01/12/2018 11:32 PM, Eddy Westbrook wrote:

> Is there already a type of 64-bit integers in the Coq standard library? Or
> at least 32-bit integers? I see some evidence of these in the documentation
> of some of the numeric modules, but I don’t really understand them…

Maybe you stumbled on the 31-bit machine integers that are used in one of the
implementations of (mathematical, arbitrary-precision) integers from Coq's
standard library. But those 31-bit integers are not really usable on their
own.

For N-bit integer arithmetic in the style of C or Java, you could use
CompCert's "Integers" library,
http://compcert.inria.fr/doc/html/Integers.html
It defines (as a parameterized module) N-bit integers and their signed and
unsigned arithmetic and logical operations, plus a whole lot of theorems
about those operations. Instantiations for N=8, N=32 and N=64 are provided,
with extra operations and theorems relating 32- and 64-bit integers.

- Xavier Leroy

[Coq-Club] 64-bit integers, Eddy Westbrook, 01/12/2018
- Re: [Coq-Club] 64-bit integers, Xavier Leroy, 01/13/2018
  - Re: [Coq-Club] 64-bit integers, Eddy Westbrook, 01/20/2018
  - Re: [Coq-Club] 64-bit integers, Vadim Zaliva, 01/25/2018