search

creusot-rs / creusot

Creusot helps you prove your code is correct in an automated fashion.
GNU Lesser General Public License v2.1
1.11k stars 51 forks source link

Support for bitwise operations #743

Open marcfir opened 1 year ago

marcfir commented 1 year ago

I am trying to verify some code that contains bitwise operations like AND, OR, SHIFT, NEGATE that are currently not supported. How much effort will it take to support these types of operations?

xldenis commented 1 year ago

This is something I would like to add proper support for soon. I think there is a low-effort, 80% solution we could provide too.

xldenis commented 1 year ago

Sorry for the delay, I'm a bit overwhelmed with ETAPS preparations right now.

I think there's a pragmatic solution which would allow you to have these operations.

  1. Add support for translating the various bitwise operators
  2. Provide an alternate prelude.mlw which uses Why3's bitwise machine integers instead of the current ones.

A complete solution would require thinking about how we want to handle the existence of mathematical integers Int?

xldenis commented 1 year ago

I can write up a PR which adds this today or by the end of the week.

marcfir commented 1 year ago

This would be a good attempt for me to test bit twiddling.

xldenis commented 1 year ago

I'll throw up a PR this week and we can test it out.