coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Lars Rasmusson <lars.rasmusson AT ri.se>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Operations on boolean vector : shift / mask
Date: Wed, 21 Feb 2018 13:59:12 +0000
Accept-language: en-US, sv-SE
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lars.rasmusson AT ri.se; spf=Pass smtp.mailfrom=lars.rasmusson AT ri.se; spf=None smtp.helo=postmaster AT se-out2.mx-wecloud.net
Ironport-phdr: 9a23:Jx7Lyx3/C/wjtkM6smDT+DRfVm0co7zxezQtwd8ZseIVLfad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmiDkJOSMl8G/ZicJwgqBUoBO9qBNw2IPUb52ZNP9kc6/BYd8WW2xMVdtRWSxbBYO8apMCAewbMuZCtIn2ukcAogGlBQmpGePv0SRIhnjw3aYn1OkhFRvJ3BY7H94UqnTbts71NKIPUeCu16nIyjPDYuhM2Tf88oTIaQ4urOiKULltf8TRzkwvGBnEjlWWsYHlPjWV1v4Ms2eB9eZgW/ivhmg6oA9yujii3sQhh43Tio4L1FzI6D91zJg1KNC4UkJ3fNypHZlIuy2HK4d6WN4uT310tCog1rEKo5+2cSoSxJQp2RHSaOCLfo2N7x/hSemcIzR1iXdmdb2inBm/8E2txvDyW8ap3lZHqylIncXQuX0P0RHY99KJReFn/ki73DaCzwDT5f9AIUAzjafbMIAuzqc3lpoOrUTPADX6mED5jaOPeEQr5PSn6+DgYrX7u5CQLYl0hR/iMqg2m8y/B/o3MhQWUmWY/emwzqPv8VPkTLlQkPE7kqnUvIrHKckZpKO1GwpV3Zwi6xa7ATemytMYnXwfIVJBYh2HlZPpN0vUIP/iFve/hkmskCxwx/DBOL3sGY/NLnnZnLf6Y7lx81RcxxYrzdBD+5JUDakML+70Wk/ordDXEhs5MxGvzOv8E9V81oYeWXqVDaODMaPSt0WI5uM1LOWWao8VomW1F/9wrfXplDoynUIXVaivx5oeLn6iVLwyKEKAJHHon90pEGEQvwN4Qva823OYVjsGQ3+oROoG7yo+FZm9CoGLEoSkmqfHxi6gG4BNfWdAIkqNV2zlIdbXE8wQYT6fd5cy2gcPUqKsHtd4hEOe8TTiwr8iFdL6vygRtJbtzt9wuL/JlFcp+G4tVpjP4yS2V2hx21gwaXouxqkg81Z8jEyOg/Ah3q5oUOdL7vYMaT8UcJ7Ry+sgV4LpV0fGY8vTDlO2B8qrCjU2U953xdISMR5w

If by "shift" you mean "rotate", perhaps you can build on 'rot1', which puts the last element first...

Require Import Vector.

Definition last_n {T m} (v:Vector.t T m) n (H:n<=m) := rev ((take n H (rev v))).

Definition rot1 {T n} (v:Vector.t T (S n)) := append (last_n v 1 (le_n_S _ _ (le_0_n _))) (take n (le_S _ _ (le_n _)) v).

On 20 Feb 2018, at 10:25 , Vincent <vincent.siles AT gmail.com> wrote:

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#

Attachment: smime.p7s
Description: S/MIME cryptographic signature

[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