coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Vincent Siles <vincent.siles AT ens-lyon.org>
To: Coq-Club Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Operations on boolean vector : shift / mask
Date: Fri, 2 Mar 2018 13:18:45 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vincent.siles AT ens-lyon.org; spf=None smtp.mailfrom=SRS0=dwKI=FY=ens-lyon.org=vincent.siles AT bounce.ens-lyon.org; spf=Pass smtp.helo=postmaster AT sonata.ens-lyon.org
Ironport-phdr: 9a23:j1gCnhBa8UkPgv1/KEr2UyQJP3N1i/DPJgcQr6AfoPdwSPX5osbcNUDSrc9gkEXOFd2Cra4c0KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUijexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0iScHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRsReVyJBDI2ybIUBEvQPMvpDoobnu1cDtwGzCRWwCO7tzDJDm3/43bc90+QkCQzJ0w0gH9QSv3vKqtX1KLoZX/20zKnM0zrDdO5d1DDj6IjJdBAuve+DXbRsccbL0kkvFgfFgUuLqYH+ITyV0P8Nv3Gf7+tgUuKvjXQrqwZrojig38ohjJTCiIwSylDB7yp5wYA1KMW5SE59e96kEYFfuzuUN4tsWs8iTGBouDo6yr0bopG3ZjQFyJMixxPZdveJcJCI7wr+WOuePTt0nnBodbClixqv8EWty/fwWtS63VtJtiZIkNbBumoQ2xDN6sWLUPhw8lm71TuP2A3e7PxPL1oumqrBMZEhx6Y9lpoNvkTHGS/7gF72jKiQdko+5uin8f7rbavgpp+HLoN0jgH/MqMomsClBuQ4KAcOU3Ca+eS6yrLj4VX0TKhFg/EqiKXUspLXKd4GqqO4AgJZyJsv5hi8Aju+1dQXh3gHLFZLeBKdiIjpPknDLu3kA/min1ihiCpkxv7DMLPiGpjDLnrMna//crZ78E5Q0Q4zzNBY55JSEL0BJ+jzWkDpudzGDx85NRC7zPjhCNVhzI8eQmOPAquHP6PJqlKH/eUvI/SKZIAJpjnxMeYq5/j1jXMgnV8cfa6p3Z0NZHC/BPRmLF2VYWDwjdcZDWcKog0+QfT2h12FSD5ffmq9X6Yh5j4gE4+mFofCRoW1gLObxiu7H5tWZnpHCl+WC3voeZ+ECL8wb3e5JdYkuTgZX/CKT5IrnUWlsxa/wL56JMLV/DcZvNTtzo4myffUkEQM9Dp/AsKBm1qMS2xv1jcWRjk90aZj51d8zlqY+aV+mLlcBNtVofRTXVFpZtbn0+VmBoWqCUr6ddCTRQPjG43+WGBjfpcK29YLJn1FNZCnhxHH0TCtBuVMxbaMGZo//+TR2WO0I9d6zTDBzqZz1wB6EPsKDnWvg+tEzyaWH5TAyhnLmqCxMKAN2yiL832MnzLX4RNoFTVoWKCAZkgxI0vbqdOjvxHZSLmnFb1hPw1ajMqTLa0Mbcfm3wxL

Hi !

Yes, I remember that `rev (rev v) = v` is kind of a Kraken for dependent types :)

I already had a look at the CompCert library, but I won't be able to use for my current project because of the license.

Thank you for the last link, I'll have a look !

Best,

2018-03-02 9:01 GMT+01:00 Pierre-Evariste Dagand <pedagand AT gmail.com>:

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