coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Operations on boolean vector : shift / mask

From: Vincent <vincent.siles AT gmail.com>
To: Coq-Club Club <coq-club AT inria.fr>
Subject: [Coq-Club] Operations on boolean vector : shift / mask
Date: Tue, 20 Feb 2018 10:25:31 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vincent.siles AT gmail.com; spf=Pass smtp.mailfrom=vincent.siles AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f50.google.com
Ironport-phdr: 9a23:yBjxlx25k86K2mZTsmDT+DRfVm0co7zxezQtwd8Zse0RLvad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7Vq4/Vyi84Kh3SR/okCYHOCA/8GHLkcx7kaZXrAu8qxBj34LYZYeYP+d8cKzAZ9MXXWpPUMhSWSJcHI2zc5ACAPAdMetCtYTxu0cCoBm4CAKxBO3v0DhIhnru0KI10uQhFx3J0xImH9ISrX/Zq8v1NKYUUe+p0qbIyynDY+lN2Tf87IjHbAshrOqDXbJ1a8XRyE0vGxnZgVWXrIzoJjWY3fkDvWic6upvT+Ovi2g/pgFwpDiv3MYshZPTioIb0FDJ8zhyzoUtJdCgSkN2bsSoHIZOuyyaLYd7Qd0uT3totSomzLANpIS1czIQyJs9wh7Sc/yHfJaM4hLkTOuRJC13hHNheL6miRey9FSsxvTyVsS0zFpGtCVFkt7LtnAC0xzc9NKLRed6/kekwTqP1gbT5f9YIU0sl6fWJIQtzqMumpcTq0jOHTH6lF/2gaOKbkkk//Kn6+XjYrXovJ+cMIp0hxngMqQvnMywHfo3Mg4SX2SB4uS81bnj8lPiQLhRgf02l7PWsJHeJcgBuqG5BApV3p456xmjFzemzMgYnX4fIV1ZfxKHlpHlNE3KIPDlFviymE+skTdux/DeJLLtGJTNLn7ZkLfgZ7lx8UBcyBBghexYsrlTE/QqJO/5EmT1qdaQWhQ+Kkm/x/vtINR7zIIXH2yVVPy3KqTX5GGJ4OkiJfXEMJEUvj3wLeRj/P/qgGQRlloUfK3v1pwSPiPrVs96KlmUNCK/yuwKFn0H609nFLSz2Q+yFAVLbnP3ZJoSozQyCYaoF4DGH9n/j7mI3SP9FZpTNDkfVgK8VEzwfoDBYM8iLTqIK5Y4wDMBXLmlDYQm0EP27VKo+/9cNuPRvxYgm9fj2dxyvbCBkBgz8XlrCpzY3TzVCW5zmWwMSnk926Ut+UE=

Hi !

I'm trying to write some properties about N bit integers in Coq (N = 54 and 27), and I am considering the 'mask' and 'left/right shifts'.

From the library [1], I see that I can use 'trunc' to implement my 'mask' operation, but I don't see anything I could use to implement 'right shift'. My first goal is to prove something like:

append (n & MASK27) (n >> 27) == n

Did I miss something in the lib or am I looking at the from library ?

Best,
V.

[1] https://coq.inria.fr/library/Coq.Vectors.VectorDef.html#

[Coq-Club] Operations on boolean vector : shift / mask, Vincent, 02/20/2018
- Re: [Coq-Club] Operations on boolean vector : shift / mask, Lars Rasmusson, 02/21/2018
  - Re: [Coq-Club] Operations on boolean vector : shift / mask, Vincent Siles, 02/21/2018
    - Re: [Coq-Club] Operations on boolean vector : shift / mask, Lars Rasmusson, 02/21/2018