Remove toNat from LLVM semantics

[tobiasgrosser]

Several LLVM functions use toNat, while they can use a bit-vector level comparison which would allow them to be bitblasted.

We should transform this code:

@[simp_llvm]
def lshr? {n} (op1 : BitVec n) (op2 : BitVec n) : IntW n :=
  let bits := op2.toNat
  if bits >= n then .none
  else pure (op1 >>> op2)

into

@[simp_llvm]
def lshr? {n} (op1 : BitVec n) (op2 : BitVec n) : IntW n :=
  let bits := op2
  if bits >= n then .none
  else pure (op1 >>> op2)

and while at it, clean it up to sth like:

@[simp_llvm]
def lshr? {n} (op1 : BitVec n) (op2 : BitVec n) : IntW n :=
  if op2 >= n then
    none
  else
    pure (op1 >>> op2)

[lfrenot]

Using BitVec.ofNat is fine, right?

[tobiasgrosser]

In which way? Why do you need it?

[lfrenot]

When you write op2 >= n in lshr, you're comparing a BitVec with a Nat I don't think this works properly But I may be wrong

[tobiasgrosser]

This should work in bv_decide.

[tobiasgrosser]

What is your concern?

[lfrenot]

This should work in bv_decide.

oh okay, then there is no issue indeed I'll do that and open a PR