coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] 16 Bit Unsigned Integer Library

From: Xavier Leroy <xavier.leroy AT college-de-france.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] 16 Bit Unsigned Integer Library
Date: Thu, 2 Dec 2021 10:16:23 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=xavier.leroy AT college-de-france.fr; spf=Pass smtp.mailfrom=xavier.leroy AT college-de-france.fr; spf=None smtp.helo=postmaster AT smtpout02-ext4.partage.renater.fr
Dkim-filter: OpenDKIM Filter v2.10.3 zmtaauth02.partage.renater.fr B3420A0D04
Ironport-data: A9a23:gdJty6ye6CSaxgXtJbd6t+cXxyrEfRIJ4+MujC/XYbTApG92gzwCnWZMWGCGOPqJZGTxe4xxYd+1oxxUvZKBztcyHQtv/xmBbVoa8JufXYzxwmTYZn7JcJWbFCqL1yivAzX5BJhcokT0+1H9bdANkVEmjfvRH+CkUradUsxMbVQMpBkJ2UoLd9ER2dYAbeiRW2thiPuqyyHtEAfNNw1cbgr435m+RCZH55wejt+3UmsWPpintHeG/5Uc4Ql2yauZdxMUSaEMdgK2qnqq8V23wo/Z109F5tKNibPnakoXXuaIeAWeliYQQ6G4nhFNq2oo36AyKPcGL0lN49mLt4kglJMX6MD2E1twePaV8Agee0Ew/yVWLaRY+bLdZ3yyq8uC50bBd3/hzPgrAExzM5cR/O16R29UnRAdAG9SP0Hc2b7eLLWTE7U915tzc6EHJrg3sXZ5iDrdEPwOWoHGW6yM5NlC3T52iNomIBp0T95BPGEpMQCZNkUJYkNNXcp4xrr22G2kJmUe9UbK8IMpx0PW6iBx9JnkFubPXMjTHZAN2h6Mzo7d13/8HgkdKcDHk3+I4m7wwPfGhz/yV49UDrC+/+Jnmhud3AQu5NQtfQPTiZGEZoSWArqz6nD4+xbCaYAp8VCzScThB0f9rW6Y4lgEUsBMGuI3rhuAzKPI7hzfCHJsovtpADA5nJdeeNDo/gbhcxDV6fhHu7qRTX+S+/KYoHa8IyETJmJEazVsoc4t/Yz4uI9q5v7QZo8LLUN25+EZ3Rn7xDSOoSczwrkeyMAR3qOw8BbJmVpAY7ChohEdvm3qY45u0u+1iENJqWBlBZg3IMus9Lqkc2Q=
Ironport-hdrordr: A9a23:PtcQcKqXb9HxxAvqnNuvkzsaV5q8eYIsimQD101hICG9E/bo6fxH/pwguSMc7Qx/ZJhOo6H6BEDtewKlyXcx2/hpAV7AZniAhILLFvAe0WKK+VSJcEeSl44ttpuIMZIObuEYZmIK8foSjjPIbOrIA+P3kpyAtKPxy39sSEVNcKFv7wBwD0K+HldtTAdLQboVfaDsnPavawDQHEj/p/7LYkUtbqz5q9rCiZ78JScaCRJi0hCHiQmj7qX3eiLoris2Ynd1zbAr7GTf1zXl6KnmieiyziXA33Lehq4m6ecJFeEsOPCx

On Thu, Dec 2, 2021 at 1:44 AM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

I am looking for 16 bit unsigned integer library in Coq and I found this library [1] but at the very top it says, “This library has been deprecated since Coq version 8.10”, so I am curious about the other alternatives.

One way, at the top of my head, I can do this by
Record UInt16 := mk_uint { val: N; 0 <= val < 2^16} and define all the needed functions and proofs but before that I would like see the existing solutions.

The Integers library in CompCert implements this approach, for any number of bits: https://compcert.org/doc/html/compcert.lib.Integers.html

To get your 16-bit integers:

Module Wordsize_16.
Definition wordsize := 16%nat.
Remark wordsize_not_zero: wordsize <> 0%nat.
Proof. unfold wordsize; congruence. Qed.
End Wordsize_16.

Module Int16 := Integers.Make(Wordsize_16).

Enjoy,

- Xavier Leroy

Best,
Mukesh

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

[Coq-Club] 16 Bit Unsigned Integer Library, mukesh tiwari, 12/02/2021
- Re: [Coq-Club] 16 Bit Unsigned Integer Library, Pierre-Yves Strub, 12/02/2021
- Re: [Coq-Club] 16 Bit Unsigned Integer Library, Xavier Leroy, 12/02/2021
  - Re: [Coq-Club] 16 Bit Unsigned Integer Library, mukesh tiwari, 12/03/2021
    - Re: [Coq-Club] 16 Bit Unsigned Integer Library, Ana Borges, 12/07/2021
      - Re: [Coq-Club] 16 Bit Unsigned Integer Library, mukesh tiwari, 12/09/2021