Feature request: bit-vector array syntax

[seanmcl]

It would be nice to be able to access bit vector fields as booleans. E.g.

var foo: bv128 = 1839428 as bv128
assert foo[17] == 1 // I'm not sure if this is true

[davidcok]

How about this syntax:

[1-9][0-9]#0-9A-Za-z

The part before the # is the radix (as a decimal number). The part after is a sequence of ‘digits’ appropriate to the radix, underscores allowed, case-insensitive, leading 0s allowed, most-significant digits to the left, no embedded white space permitted.

• David

On Apr 9, 2021, at 2:58 PM, Sean McLaughlin @.***> wrote:

It would be nice to be able to access bit vector fields as booleans. E.g.

var foo: bv128 = 1839428 as bv128 assert foo[17] == 1 // I'm not sure if this is true — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/dafny-lang/dafny/issues/1175, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABITDQASEEHZXRNK23RI4FDTH5E5ZANCNFSM42VQEI5Q.

[RustanLeino]

These are two distinct proposal, methinks. @seanmcl is proposing a syntax foo[17] that tells you whether or not bit 17 of bitvector foo is a 1. @davidcok is proposing an extended syntax for numeric literals (in addition to the decimal and hexadecimal forms that are supported today).

[davidcok]

Sure. My first thought was that Sean wanted to tell at a glance what a given bit value of a literal is. But the array element syntax is useful here as well

On Apr 9, 2021, at 3:53 PM, Rustan Leino @.***> wrote:

These are two distinct proposal, methinks. @seanmcl https://github.com/seanmcl is proposing a syntax foo[17] that tells you whether or not bit 17 of bitvector foo is a 1. @davidcok https://github.com/davidcok is proposing an extended syntax for numeric literals (in addition to the decimal and hexadecimal forms that are supported today).

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/dafny-lang/dafny/issues/1175#issuecomment-816931800, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABITDQF7MI4G4ISADQ3Q7BDTH5LMBANCNFSM42VQEI5Q.

[robin-aws]

Would the type of foo[17] be boolean or int? I think we're implying the latter, I just ask because the original comment says "booleans".

[seanmcl]

I'd want it to be boolean. Otherwise we'd need a painful extra != 0 check.

[RustanLeino]

I too think it bool is good. If you want the result to be a bitvector, you'd still need to write foo & (1 << 17).

I could also see use for the companion operation foo[n := b], which says to set bit n if b evaluates to true to and clear bit n otherwise. Again, b would be a bool.

[seanmcl]

Yeah, we have the foo[n := b] operator defined in our code, so that would be a nice addition as well.