feat: add udiv/umod bitblasting for bv_decide (#5281)

This PR adds the theorems

```
@[simp]
theorem divRec_zero (qr : DivModState w) :
  divRec w w 0 n d qr  = qr

@[simp]
theorem divRec_succ' (wn : Nat) (qr : DivModState w) :
    divRec w wr (wn + 1) n d qr =
    let r' := shiftConcat qr.r (n.getLsbD wn)
    let input : DivModState w :=
      if r' < d then ⟨qr.q.shiftConcat false, r'⟩ else ⟨qr.q.shiftConcat true, r' - d⟩
    divRec w (wr + 1) wn n d input
```

The final statements may need some masasging to interoperate with
`bv_decide`. We prove the recurrence for unsigned division by building a
shift-subtract circuit, and then showing that this circuit obeys the
division algorithm's invariant.

--- 

A `DivModState` is lawful if the remainder width `wr` plus the dividend
width `wn` equals `w`,
and the bitvectors `r` and `n` have values in the bounds given by
bitwidths `wr`, resp. `wn`.
This is a proof engineering choice: An alternative world could have
`r : BitVec wr` and `n : BitVec wn`, but this required much more
dependent typing coercions.
Instead, we choose to declare all involved bitvectors as length `w`, and
then prove that
the values are within their respective bounds.

---------

Co-authored-by: Tobias Grosser <[email protected]>
Co-authored-by: Alex Keizer <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: Tobias Grosser <[email protected]>

src/Init/Data/BitVec/Basic.lean

@@ -676,6 +676,13 @@ result of appending a single bit to the front in the naive implementation).
     That is, the new bit is the least significant bit. -/
 def concat {n} (msbs : BitVec n) (lsb : Bool) : BitVec (n+1) := msbs ++ (ofBool lsb)
 
+/--
+`x.shiftConcat b` shifts all bits of `x` to the left by `1` and sets the least significant bit to `b`.
+It is a non-dependent version of `concat` that does not change the total bitwidth.
+-/
+def shiftConcat (x : BitVec n) (b : Bool) : BitVec n :=
+  (x.concat b).truncate n
+
 /-- Prepend a single bit to the front of a bitvector, using big endian order (see `append`).
     That is, the new bit is the most significant bit. -/
 def cons {n} (msb : Bool) (lsbs : BitVec n) : BitVec (n+1) :=