Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
    < Chronological >      < Thread >
  • From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] 16 Bit Unsigned Integer Library
  • Date: Fri, 3 Dec 2021 10:14:20 +1100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f46.google.com
  • Ironport-data: A9a23:TExAoK4m5RlGzYVKujpWCgxRtFHGchMFZxGqfqrLsXjdYENS1z0GyDQWXjuOOP2LMGOmLYhwPYzi8EwB7ZGAyt81QQMd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t63yUjRxRSwNZie0SiyFb/6x8hGQ6YnSHuClUbScYHgqLeNZYH5JZSxLy7ZRbrFA2oDR7zOl4bsekuWHULOX82Yc3lE8t8pvnChSUMHa41v0iLCRicdj5zcyn1FNZH4WyDrYw3HQGuG4FcbiLwrPIS3Qw4/Xw/stIovNfrfTd0QLRvvfMVHLhCYIHaelhRdGq2o51aNT2Pg0Mx8GzWXU2YopmJMR6/RcSi9xVkHIsOEAUBRDEz1/IqRc+fnGIHmjtOScykTHdz3nxPAG4EQebdVDp7kvUQmi8tRBcGxXBvyZvMq9x6v+Qe1xjOw4PczzNcUevGthxHfXF54brTrrV/2fv5kHyG5l3oYWCayLP4xDOGs2eE+VO1sSLghCIYwat+KMqnnbUjR+lEixm6sS9zGLmVE1gKyF3MH9f9WLQYBYkh/dqD6YuWv+BR4eOZqUzj/tz55lvceX9QuTZW7YPOTQGj9WbFyvKqg7DRQXUR62raD8hBLgHd1YLEMQ92wlqq1aGImDJjXid0XQnZJGlkd0txls/ykS5wSEy66S6AGcboTBZiAUc8Qo7afaWhRzvmJkXLrV6fhHv7icSHbb/bCRxd93EUD5MkdaDRI5ocA5DxUPbW39Yt8jjjquLUJtsuDIJA==
  • Ironport-hdrordr: A9a23:1Q5IWqGy+WasOPWDpLqE/8eALOsnbusQ8zAXPiFKOHhom6mj/fxG885rsCMc5AxhO03I4OrtBEDiex3hHPxOjrX5VI3KNGTbUQ2TTb2KhbGI/9SKIU3DH4BmpMVdT5Q=
  • Ironport-phdr: A9a23:MeGfyR0t75l+Lur8smDOCwQyDhhOgF0UFjAc5pdvsb9SaKPrp82kYBaGo6szxweUFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoVJ8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9qq2+yo+pDeYgpEiCa9bLhvMBi4sALdu9UMj4B/MKgx0BzJonVJe+RS22xlIE+Ykgj/6Mmt4pNt6jxctP09+cFOV6X6ZLk4QqdDDDs6KWA15dbkugfFQACS+3YTSGQWkh5PAwjY8BH3W4r6vyXmuuZh3iSRIMv7Rq02Vzu/9admUBDniCkFODA5/m/ZidF+grxHrx+6vRNz35TZbZuJOPZifK7Qe84RS2pbXsZWUixMGoa8b5YMD+UfJuZYr5T2p0cPrRqwHwasHuLvwSJPi3/zwK060PouERrG3Aw8HtIPvm7brM/0NKsIUOC1zajIzSnGb/5N1jf97ZLHchElof2WQb1wds/RxFApGgjYgVqetZbrMCmJ1uQRrWeb9exgWPqhhWMptwx8oySjy8Uxh4TUho8Z1kzI+CV3zos0OdC0VU52bNG6HZdOqyyXOYh7TMw8T29opCs21KALtYKmcSQXzpks2hDRa/uCc4eS4xLjUv6cLit/hHJgYLKwmwi98VK8yuHmUcm0yllKojJEktnKrHAN1gbc5tKJSvtn+EqqxDWB1xjL5+1aPUw5kbDXJp0hz7IqiJYfrUfOEjX5lUj3iqKda18q9fKy6+v9Z7Xrvp+cOJFwigH5Kqkun9awAeU8MgQXQWeU5Pmw2KTt/UD2QbhGlPI2kq7esJDVIcQUuLS1DBNS0oYm8xq/DjGm38oEnXQfMl5JZBaKg5LqNlzOOvz0E+uzjle2nDpkxv3KJrjhDY/MLnjHnrfhZ7F960tExQo20NBf5IxbCqoBIPLvW0/wusbXDgU4MwCuwubnCdR91p8bWW+UDa+ZNbndsV6M5u41P+aMY4oVtC7nK/c5//7ukWM5mVgFcKa12psXcWm0EehiI0WEenXhmcwBEGcPvgomVuPmklyCUThJZ3azRa0w/D87CJj1RbvEE4uqmfmK2DqxNpxQfGFPTF6WQlnycIDRXuoPZTmSatNgjTUeVPD1TpIi2AquqA7lwqBmaOvV+zEdnZ3m3dlxoebUkEdhpnRPE82B3jTVHClPlWQSSmputEieiUl0y1PG3KQhxvIES5pc4PRGVgp8PpnZnbQS4z/aVQfIf9PPQ1GjEIzO6dQZQdc4wttIaEF4SY3Ksw==
Thank you very much Pierre and Xavier. It’s very helpful. 

Best,
Mukesh 

On Thu, 2 Dec 2021 at 8:17 pm, Xavier Leroy <xavier.leroy AT college-de-france.fr> wrote:
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

Archive powered by MHonArc 2.6.19+.

Top of Page