BitsTricksSlow.scala

/* Copyright 2009-2021 EPFL, Lausanne */

import stainless.lang._
import stainless.annotation._

object BitsTricksSlow {

  def bitAt(x: Int, n: Int): Boolean = {
    require(n >= 0 && n < 32)
    ((x >> n) & 1) == 1
  }

  def isBitNSet(x: Int, n: Int): Int = {
    require(n >= 0 && n < 32)
    (x & (1 << n))
  }

  def toggleBitN(x: Int, n: Int): Int = {
    require(n >= 0 && n < 32)
    x ^ (1 << n)
 }.ensuring(res => 
      if(isBitNSet(x, n) != 0) isBitNSet(res, n) == 0
      else isBitNSet(res, n) != 0)

  def turnOffRightmostOneRec(x: Int, indexFromLeft: Int): Int = {
    require(0 <= indexFromLeft && indexFromLeft < 32)
    if(bitAt(x, 31 - indexFromLeft)) toggleBitN(x, 31 - indexFromLeft)//(x ^ (1 << (31 - indexFromLeft)))
    else if(indexFromLeft == 0) x
    else turnOffRightmostOneRec(x, indexFromLeft - 1)
  }

  // proves in 10s
  def turnOffRightmostOne(x: Int): Int = {
    x & (x - 1)
 }.ensuring(_ == turnOffRightmostOneRec(x, 31))

  // 010100 -> 010111
  def rightPropagateRightmostOne(x: Int): Int = {
    x | (x - 1)
  }

  def property1(x: Int): Boolean = {
    val y = rightPropagateRightmostOne(x)
    y == rightPropagateRightmostOne(y)
 }.ensuring(b => b)

  def isRotationLeft(x: Int, y: Int, n: Int, i: Int): Boolean = {
    require(0 <= i && i < 32 && 0 <= n && n < 32)
    val isOk = bitAt(x, i) == bitAt(y, (i + n) % 32)
    if (i == 0) isOk else isOk && isRotationLeft(x, y, n, i-1)
  }

  //rotateLeft proves in 1 minute (on very powerful computer)
  def rotateLeft(x: Int, n: Int): Int = {
    require(n >= 0 && n < 32)
    val front = x >>> (32 - n)
    (x << n) | front
 }.ensuring(res => isRotationLeft(x, res, n, 31))

  //careful with overflows, case definition, truncated
  def safeMean(x: Int, y: Int): Int = {
    if(x >= 0 && y <= 0 || x <= 0 && y >= 0) (x + y)/2
    else if(x >= 0 && x <= y) x + (y - x)/2
    else if(x >= 0 && y <= x) y + (x - y)/2
    else if(x <= 0 && x <= y) y + (x - y)/2
    else x + (y - x)/2
  }

  //proves in 45 seconds
  def magicMean(x: Int, y: Int): Int = {
    val t = (x&y)+((x^y) >> 1)
    t + ((t >>> 31) & (x ^ y))
 }.ensuring(res => res == safeMean(x, y))


}