Bitvectors using too much time/resources

[seanmcl]

Dafny version

4.5

Code to produce this issue

type shorts8 = (bv16,bv16,bv16,bv16,bv16,bv16,bv16,bv16) 

  opaque ghost function IpV6BitsToShorts(br: bv128): shorts8
  {
    var b0 := ((br >> 112) & 0xffff) as bv16;
    var b1 := ((br >> 96) & 0xffff) as bv16;
    var b2 := ((br >> 80) & 0xffff) as bv16;
    var b3 := ((br >> 64) & 0xffff) as bv16;
    var b4 := ((br >> 48) & 0xffff) as bv16;
    var b5 := ((br >> 32) & 0xffff) as bv16;
    var b6 := ((br >> 16) & 0xffff) as bv16;
    var b7 := ((br >>  0) & 0xffff) as bv16;
    (b0, b1, b2, b3, b4, b5, b6, b7)
  }

  opaque ghost function IpV6ShortsToBits(shorts: shorts8): bv128
  {
    var (s0, s1, s2, s3, s4, s5, s6, s7) := shorts;
    var b0 := (s0 as bv128) << 112;
    var b1 := (s1 as bv128) << 96;
    var b2 := (s2 as bv128) << 80;
    var b3 := (s3 as bv128) << 64;
    var b4 := (s4 as bv128) << 48;
    var b5 := (s5 as bv128) << 32;
    var b6 := (s6 as bv128) << 16;
    var b7 := (s7 as bv128) << 0;
    var br := b0 | b1 | b2 | b3 | b4 | b5 | b6 | b7;
    br
  }

// Dafny has a lot of trouble managing this, even with opaqueness
  lemma IpV6ShortsToBitsEq(shorts: shorts8)
    ensures IpV6BitsToShorts(IpV6ShortsToBits(shorts)) == shorts
  {
    var (s0, s1, s2, s3, s4, s5, s6, s7) := shorts;
    var b0 := (s0 as bv128) << 112;
    var b1 := (s1 as bv128) << 96;
    var b2 := (s2 as bv128) << 80;
    var b3 := (s3 as bv128) << 64;
    var b4 := (s4 as bv128) << 48;
    var b5 := (s5 as bv128) << 32;
    var b6 := (s6 as bv128) << 16;
    var b7 := (s7 as bv128) << 0;
    var br := b0 | b1 | b2 | b3 | b4 | b5 | b6 | b7;
    // Easy for Dafny
    assert br == IpV6ShortsToBits(shorts) by { reveal IpV6ShortsToBits(); }

    var s0' := ((br >> 112) & 0xffff) as bv16;
    var s1' := ((br >> 96) & 0xffff) as bv16;
    var s2' := ((br >> 80) & 0xffff) as bv16;
    var s3' := ((br >> 64) & 0xffff) as bv16;
    var s4' := ((br >> 48) & 0xffff) as bv16;
    var s5' := ((br >> 32) & 0xffff) as bv16;
    var s6' := ((br >> 16) & 0xffff) as bv16;
    var s7' := ((br >>  0) & 0xffff) as bv16;
    var s := (s0', s1', s2', s3', s4', s5', s6', s7');

    // Hard for dafny, tons of resources, ~20 seconds
    assert IpV6BitsToShorts(br) == s by { reveal IpV6BitsToShorts(); }

    assume {:axiom} false;
  }

Command to run and resulting output

No response

What happened?

I expected this to pass instantly. Instead it takes 20 seconds and ~25M resources. This makes working with bitvectors difficult.

What type of operating system are you experiencing the problem on?

Mac

[keyboardDrummer]

I'm guessing this is rather difficult to resolve. @seanmcl could you quantify how badly this is affecting you?

[atomb]

I think this won't be trivial to resolve, as it will require changing how we generate verification conditions. However, we are incrementally making steps toward that, though I'm not sure offhand how long it'll take to get to where this sort of thing will be easier to prove. Even so, it's very useful to have concrete examples to test with as we progress.

[seanmcl]

It's a bummer. I think we can fumble our way around it.