Extern Specs for Bitwise Operands on Ints

[vrindisbacher]

It seems that at the moment, going from integers to bitvectors and back to reason about certain bit operands is not possible. For example, the following does not work:

flux_rs::defs! {
    fn negated(x: int) -> int {
        bv_bv32_to_int(bv_not(bv_int_to_bv32(x)))
    }
}

#[flux_rs::sig(fn (u32[@x]) -> u32[negated(x)])]
fn negated(x: u32) -> u32 {
    !x
}

I'm assuming that this is because there is no refinement for Not on u32's?

If so, I think it would be great to add this to Flux itself. I know that @nilehmann mentioned he wanted to do this with extern specs needed in VTock at one point.

I need to add refinements for most of the bit operands, and I'm happy to do this somewhere other people can use it? This could probably be implemented fairly easily (for int types at least) by using macros similar to those Rust use (See here and here)

[nilehmann]

The issue here is that ! (and all bitwise operators) are primitive operations. The type of primitive operations is hardcoded here

flux/crates/flux-refineck/src/primops.rs

Line 386 in ddb4935

fn mk_not_rules() -> RuleMatcher<1> {

. We could easily hardcode ! to have type fn(x: u32) -> u32[bv_bv32_to_int(bv_not(bv_int_to_bv32(x)))], but I'm not sure that's what we want because the cost of bitvectors is high. I think it's also not enough because if you are mixing various bitwise operations you want to do the entire computation in bitvectors and only go back to ints at the end. I wish we had a way in which you can locally opt-in to bit vectors.

The best idea I have so far is to define a (trusted) wrapper around u32 that overloads all arithmetic operations with bit-vector semantics. You would explicitly go from u32 to the wrapper, do operations in bitvector land, and then explicitly go back to int again.

[vrindisbacher]

@nilehmann, the wrapper seems interesting. Are you thinking something along these lines?

use std::ops::{BitAnd, Not};

flux_rs::defs! {
    fn bv32(val: int) -> bitvec<32> {
        bv_int_to_bv32(val)
    }

    fn int(val: bitvec<32>) -> int {
        bv_bv32_to_int(val)
    }

    fn not(val: bitvec<32>) -> bitvec<32> {
        bv_not(val)
    }

    fn and(val1: bitvec<32>, val2: bitvec<32>) -> bitvec<32> {
        bv_and(val1, val2)
    }
}

#[flux_rs::opaque]
#[flux_rs::refined_by(x: bitvec<32>)]
pub struct B32(u32);

impl From<u32> for B32 {
    #[flux_rs::trusted]
    #[flux_rs::sig(fn (u32[@val]) -> B32[bv32(val)])]
    fn from(value: u32) -> B32 {
        B32(value)
    }
}

impl Into<u32> for B32 {
    #[flux_rs::trusted]
    #[flux_rs::sig(fn (B32[@val]) -> u32[int(val)])]
    fn into(self) -> u32 {
        self.0
    }
}

impl Not for B32 {
    type Output = B32;

    #[flux_rs::trusted]
    #[flux_rs::sig(fn (B32[@x]) -> B32[not(x)])]
    fn not(self) -> B32 {
        B32(!self.0)
    }
}

impl BitAnd for B32 {
    type Output = B32;

    #[flux_rs::trusted]
    #[flux_rs::sig(fn (B32[@x], B32[@y]) -> B32[bv_and(x, y)])]
    fn bitand(self, rhs: Self) -> B32 {
        B32(self.0 & rhs.0)
    }
}

#[flux_rs::sig(fn (u32[@x], u32[@y]) -> u32[int(not(and(bv32(x), bv32(y))))])]
fn some_bitwise_op(x: u32, y: u32) -> u32 {
    (!(B32::from(x) & B32::from(y))).into()
}

[vrindisbacher]

I think this is kind of nice, but I really don't like how verbose B32::from and .into() are. Also, if you wanted to run this program, would all that code get eliminated? I'm assuming yes but would be nice to see if that's actually the case.

[vrindisbacher]

@nilehmann, I have a file that implements bitwise operands for most types (see below). Is this something we could include in a flux-support crate? I can open a PR into that if you think it's useful.

use std::ops::{BitAnd, BitOr, Not, Shl, Shr};

macro_rules! bitops_wrapper_def {
    ($($name:ident, $type:ty, $bits:literal)*) => ($(
        #[flux_rs::refined_by(b: bitvec<$bits>)]
        pub struct $name($type);
    )*)

}

bitops_wrapper_def! {
    B8, u8, 8
    B16, u16, 16
    B32, u32, 32
    B64, u64, 64
    B128, u128, 128
    Bi8, i8, 8
    Bi16, i16, 16
    Bi32, i32, 32
    Bi64, i64, 64
    Bi128, i128, 128
}

macro_rules! not_impl {
    ($($name:ident, $t:ty)*) => ($(
        impl Not for $t {
            type Output = $t;

            #[flux_rs::trusted]
            #[flux_rs::sig(fn ($t[@b]) -> bv_not(b))]
            #[inline]
            fn not(self) -> $t { $name(!self.0) }
        }
    )*)
}

not_impl! { B8, B8 B16, B16 B32, B32 B64, B64 B128, B128 Bi8, Bi8 Bi16, Bi16 Bi32, Bi32 Bi64, Bi64 Bi128, Bi128 }

macro_rules! and_impl {
    ($($name:ident, $t:ty)*) => ($(
        impl BitAnd for $t {
            type Output = $t;

            #[flux_rs
            #[flux_rs::sig(fn ($t[@b1], $t[@b2]) -> bv_and(b1, b2))]
            #[inline]
            fn bitand(self, rhs: $t) -> $t { $name(self.0 & rhs.0) }
        }
    )*)
}

and_impl! { B8, B8 B16, B16 B32, B32 B64, B64 B128, B128 Bi8, Bi8 Bi16, Bi16 Bi32, Bi32 Bi64, Bi64 Bi128, Bi128 }

macro_rules! or_impl {
    ($($name:ident, $t:ty)*) => ($(
        impl BitOr for $t {
            type Output = $t;

            #[flux_rs::trusted]
            #[flux_rs::sig(fn ($t[@b1], $t[@b2]) -> bv_or(b1, b2))]
            #[inline]
            fn bitor(self, rhs: $t) -> $t { $name(self.0 | rhs.0) }
        }
    )*)
}

or_impl! { B8, B8 B16, B16 B32, B32 B64, B64 B128, B128 Bi8, Bi8 Bi16, Bi16 Bi32, Bi32 Bi64, Bi64 Bi128, Bi128 }

macro_rules! shl_impl {
    ($($name:ident, $t:ty)*) => ($(
        impl Shl for $t {
            type Output = $t;

            #[flux_rs::trusted]
            #[flux_rs::sig(fn ($t[@b1], $t[@b2]) -> bv_shl(b1, b2))]
            #[inline]
            fn shl(self, rhs: $t) -> $t { $name(self.0 << rhs.0) }
        }
    )*)
}

shl_impl! { B8, B8 B16, B16 B32, B32 B64, B64 B128, B128 Bi8, Bi8 Bi16, Bi16 Bi32, Bi32 Bi64, Bi64 Bi128, Bi128 }

macro_rules! shr_impl {
    ($($name:ident, $t:ty)*) => ($(
        impl Shr for $t {
            type Output = $t;

            #[flux_rs::trusted]
            #[flux_rs::sig(fn ($t[@b1], $t[@b2]) -> bv_shl(b1, b2))]
            #[inline]
            fn shr(self, rhs: $t) -> $t { $name(self.0 >> rhs.0) }
        }
    )*)
}

shr_impl! { B8, B8 B16, B16 B32, B32 B64, B64 B128, B128 Bi8, Bi8 Bi16, Bi16 Bi32, Bi32 Bi64, Bi64 Bi128, Bi128 }

[nilehmann]

@vrindisbacher awesome! I think this is generally useful and isolated so we can "upstream" it to flux_rs. I always meant for flux_rs to be sort of like flux standard library and this falls into this category. Feel free to open a PR.

[vrindisbacher]

Sounds good! I'll open a PR. Is there a good place to put it?

[nilehmann]

This is the first time we do this so there's no precedence...

I'd add a module to flux_rs. I don't know about the name, maybe bitvec. Then people can use it as

use flux_rs::bitvec::B32

fn foo(x: B32, y: B32) -> B32 {
    !x >> y
}