coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre-Evariste Dagand <pedagand AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Operations on boolean vector : shift / mask
Date: Fri, 2 Mar 2018 09:01:43 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pedagand AT gmail.com; spf=Pass smtp.mailfrom=pedagand AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f181.google.com
Ironport-phdr: 9a23:2c3OHxOa3gD7ApZ+07El6mtUPXoX/o7sNwtQ0KIMzox0Lfv4rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgFOT438G/ZhM9tgqxFvB2svAB/z5LObY2JKPZyYqHQcNUHTmRBRMZRUClBD5umYYsOEeUBJ/xYoJfkq1UBsxuxHxOsBOL0yj9UmHD9wKM03P4uEQ7c2gwvAs8FvXPMrNrrKagdS++1w7POzTredP5W1jL955LJchAlu/2DQbVwcc/IxEQpCgjLgFKQqYn/MDOU0OQAq2mb7+x6VeKukWErsQ9xoiK3yscji4nJmoIVyk3f+ilj3Ik1Iti4RUhmatCnCJtdrz+WO5dyT884QGxluDw2xqAHtJKmZiQG1ZcqywPZZveaaYaH+AjjW/yUITpghHJqZra/hxGq/Eil0OL8V8203E9KrytLjtXAr34N2wHQ58SaUPd98UCh2TGA1wDX9O5IO1w7la3eK5I5w74wkIQcsVjbEyPohEn7iLWae0Yk9+Sy9ujqY6jqqoWBO4J3lw3yKqEulda+AeQ8PAgORW+b+eGk2b3740L2Xa9FjvIsnanfrZ/XPssbpqujDA9U1oYv8QqwDzCj0NgAh3kIMEpFeA6bj4juI1zBPPf4De6mj1uwlDdr2uvJM6b6ApTNK3jDiK3ucax8605a0gozzMpQ64haCrEbc7rPXRr6s8WdBRskOSS1xfzmAZNzzNAwQ2WKV5eYPbnIvBql+Os1IvKQacc5sTn0LfRts+bjgXY2kFkRVaas1JoTLnu/G6I1cA2ifXPwj4JZQi8xtQ0kQbmy0QzQYXtof3+3GpkEyHQ+AYOiA53EQ9n00rOE1Sa/WJZRYzIfUwzeITLTb4yBHsw0RmeKOMY4y24LULGgT8kq0hT87FanmYoiFfLd/2gjjbym1NVx4LeNxxQ79DgxHtvFlm/UHzgykWQPSDs7mqt4pB4lxw==

Hi Vincent,

> 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'.
> [...]
> [1] https://coq.inria.fr/library/Coq.Vectors.VectorDef.html#

AFAIK, Coq.Vectors is a proof-of-concept but it is not actually
"usable" in today's Coq. Emilio has this "do or dare" game where he
asks you to prove that "rev (rev v) = v", which often results in
someone badmouthing dependent types.

For a usable model of bitvectors, there is the tried-and-trusted

https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v

and some more experimental/unfinished business:

https://github.com/ejgallego/ssrbit/

Hope this helps,

--
Pierre

Re: [Coq-Club] Operations on boolean vector : shift / mask, Pierre-Evariste Dagand, 03/02/2018
- Re: [Coq-Club] Operations on boolean vector : shift / mask, Vincent Siles, 03/02/2018
  - Re: [Coq-Club] Operations on boolean vector : shift / mask, Frédéric Blanqui, 03/02/2018
  - Re: [Coq-Club] Operations on boolean vector : shift / mask, Samuel Gruetter, 03/03/2018