BitVec representations

Stream: lean4

[Alexandre Rademaker]

I am trying to understand the BitVec type.

#eval 0b0010010 -- 18
#eval 0b0010010 |>.toDigits (base := 2) -- ['1', '0', '0', '1', '0']

Is there a more straightforward way to represent 0b0010010 or 18 as 0b0010010? The literal 0b... preserving the leading zeros?

[Edward van de Meent]

i'd just like to point out that the code you're using here are not automatically BitVecs, they are just a different way to write number literals. In this case, just like writing 18 without type ascriptions, they will be interpreted as Nat.

[Edward van de Meent]

in order to get something different, try (0b0010010 : BitVec 8)

[Alexandre Rademaker]

Thanks @Edward van de Meent , I got your point. Indeed, if I use #eval (0b0010010 : BitVec 8) I will get back 0x12#8 (hexadecimal representation) but I would like to have same literal 0b0010010 printed.

To give more context:

def zones := #[2,1,2,3,3,1,3,3,0,0,2,2,0,1,0,1]

def zoneMask (as : Array Nat) (zone : Nat) : BitVec 16 :=
  as.zipIdx.foldl (λ bv p =>
    if p.1 = zone then
      bv ||| BitVec.ofNat 16 (1 <<< (15 - p.2))
     else
      bv
  ) (0 : BitVec 16)

#eval zoneMask zones 0 |>.toNat.toDigits (base := 2) -- ['1', '1', '0', '0', '1', '0', '1', '0']

It would be nice to have back 0b0000000011001010 so that the 1's are in the same positions as the zeros in the zones array. I understand that the leading zeros can be challenging to preserve in the canonical representation of a literal in binary notation... So maybe I need my own alternative to toDigits?

[Edward van de Meent]

yes, i think so... here's the best i could come up with:

def BitVec.toBinary {n : Nat} (v : BitVec n) := String.mk ((v.toFin.val.toDigits (base := 2)).leftpad n '0')

[Edward van de Meent]

you could probably use that to make a local higher priority instance of Repr (BitVec n)

[Alexandre Rademaker]

Thank you