coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre-Yves Strub <pierre-yves AT strub.nu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] 16 Bit Unsigned Integer Library
Date: Thu, 2 Dec 2021 10:00:36 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre-yves AT strub.nu; spf=Pass smtp.mailfrom=pierre-yves AT strub.nu; spf=None smtp.helo=postmaster AT mail-ed1-f47.google.com
Ironport-data: A9a23:N86mBKw3kaBTDX8zb356t+dQxyrEfRIJ4+MujC/XYbTApGwj1TcGmmMXUW/QbveDamDye9hxPoi+9hwDuseAxt9rOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA/3z27AsFehsJpPnjkrrYueJQUVUj/nSH+OmULScY0ideCc9IMsfoUI78wIGqtUw6TSJK1vlVeLa+6UzCnf9s9JHGj58B5a4lf9alK+aVAX0EbAJTasjUFf2zxH5BX+ETE27ByOQroJ8RoZWSwtfpYxV8F81/z91Yj+kurPyc0lPT7KLeAbS1TxZXK+thhUErSs3uko5HKBEOAEH1nPTx4A3lIolWZ+YEW/FOoXUmekHSRQdAj9zJoVd5KXaKz65rKR/ymWZLCq1m64/ZK0xFdRAprwf7Xt13fcfMXUGag2Jr/mnxaqyDOhqnMUqasfxVL7zEFl0lWSDS6kyGMWbBf3ev4oAmm1h15laRqOGIZcNNm9GcjDrZjljOnM2AbQChsOWh1zrKmUN9hbKscLb+EDWxQ11lbXhaZ/bJoPMSsJSkUKV4GnB+gzE7tghHIT34VK4HriE34cjXB8XWb7+0JW9//9uxVCfnykdVEJQWly8rv20zEW5Xrqz7mR8FjUG9cAPGI6DF7ERnCFUZFafogQBUZxWDoXWLSmTn7HM7V/x6ncsF1Z8hR9PiCPybSc2zEKD2dX0bdCqmNV5VlrFnoqpQfiO1eT54IPMieLojefI3jU7nLwOsw==
Ironport-hdrordr: A9a23:4Qy6mKqJtFmoZ4cefRmNBykaV5ogeYIsimQD101hICG9vPb1qynOppQmPHDP4wr5NEtLpTniAsi9qBHnmqKdiLN5VYtKNzOJhILcFvAG0WKU+UyFJ8SRzINgPN9bAspD4YrLfDtHsfo=
Ironport-phdr: A9a23:AUCUDRaEQli7xHg/cJMYaGj/LTHq0IqcDmcuAnoPtbtCf+yZ8oj4OwSHvLMx1gaPA9mQsqgUw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PObwlShTewbrx+IAiooQjSq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/27ZisNyjKxVrhGvqQFhzYHIb4+YL+Z+frrHcN8GWWZNQsRcWipcCY28dYsPCO8BMP5CoYn8uVQOtwG+Che1COzt1D9HmGT21rAn3eQ9CwHGwRcvFM8JvXTMrdX6Kr0SUfqrw6XRzTTDce1Z2Szm5YjTbhAhu+yMUqlqfcrX1EkiDgXIhUifpoL5JT2azPgNs3SF4Op6U+Kik24ppx9trzWu2MsglpTFiI0Lxl3L+ih3zok4KNK2RUJnfdOpDJ9duSGeOoZyQc4vQX1ktik1xLAYtpO2YjYGxYkhyhXCZfKHdI2I7QjiVOaXOTp4i3NleK6/hxav6kes0PHzVs6x0FpSrypFlMPMtnEX2BDJ5MiHUP1w9Vqi1zaXzw3f9P1ILEQumafYK5Mt2KA8moYQvEjZESL7mkP7h7KMeEo+4Oin8eHnb63mppCCM490jRnzMqE0lcy+BeQ0KxYBUHWG9eil2r3u8k/0TK9Fjv0xlanZv5TaKtoBqqGlBA9V154v6xe5Dzi4zNQVhWcLIE5BdR6djIXkO0vCLO7kAfq8mVihnzVmy+jDPrL7A5XNKnbDkK3mfbZ480Nc0Aszws5F55JOFL4NOfLyWlHvu9zDFRI5KBC0w/z6CNpmzI8eX3+PDreDMKzOqV+I+v4vI+6UaYAJvzb9MuEp6OLqjX8kglAQZrKp3JsSaHCgBPtqOUSZYXz2gtcAC2gGpAQ+TPa5wGGFBDVUfjO5W782zjA9EoOvS4nZFa63h7nU5Ca2BIdbI1FYB0vEKmvyao/MD+8NZTiIL4pwjDEffaO9UZIrkxez4lypg4F7J/bZr3VL/ano08J4srW7ffAa8DV1C4GQ3zjIQT0r2GwPQDAy0eZ0pkkvkj9rNIBjn+ZFH5pV+qEROu/VHYXA1fFwTdbvCFupQw==

Hi,

In the Jasmin project, we are using this:

https://github.com/jasmin-lang/coqword

Best, Pierre-Yves.

Le jeu. 2 déc. 2021 à 01:44, mukesh tiwari
<mukeshtiwari.iiitm AT gmail.com> a écrit :
>
> 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.
>
> 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