This PR adds a BitVec lemma that `(x >> x) = 0` and plumbs it through to
bv_normalize. I also move some theorems I found useful to the top of the
ushiftRight section.
This PR adds a number of simple comparison lemmas to the top/bottom
element for BitVec. Then they are applied to teach bv_normalize that
`(a<1) = (a==0)` and to remove an intermediate proof that is no longer
necessary along the way.
This PR adds lemmas to rewrite
`BitVec.shiftLeft,shiftRight,sshiftRight'` by a `BitVec.ofNat` into a
shift-by-natural number. This will be used to canonicalize shifts by
constant bitvectors into shift by constant numbers, which have further
rewrites on them if the number is a power of two.
This PR adds rewrites that normalizes left shifts by extracting bits and
concatenating zeroes. If the shift amount is larger than the bit-width,
then the resulting bitvector is zero.
```lean
theorem shiftLeft_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) : x <<< n = 0#w
theorem shiftLeft_eq_concat_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
x <<< n = ((x.extractLsb' 0 (w-n)).append (BitVec.zero n)).cast (by omega)
```
This PR supports rewriting `ushiftRight` in terms of `extractLsb'`. This
is the companion PR to #6743 which adds the similar lemmas about
`shiftLeft`.
```lean
theorem ushiftRight_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) :
x >>> n = 0#w
theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
x >>> n = ((0#n) ++ (x.extractLsb' n (w - n))).cast (by omega)
```
This PR adds the lemmas that show what happens when multiplying by
`twoPow` to an arbitrary term, as well to another `twoPow`.
This will be followed up by a PR that uses these to build a simproc to
canonicalize `twoPow w i * x` and `x * twoPow w i`.
This PR defines `reverse` for bitvectors and implements a first subset
of theorems (`getLsbD_reverse, getMsbD_reverse, reverse_append,
reverse_replicate, reverse_cast, msb_reverse`). We also include some
necessary related theorems (`cons_append, cons_append_append,
append_assoc, replicate_append_self, replicate_succ'`) and deprecate
theorems`replicate_zero_eq` and `replicate_succ_eq`.
---------
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Kim Morrison <kim@tqft.net>
This PR adds a `toFin` and `msb` lemma for unsigned bitvector modulus.
Similar to #6402, we don't provide a general `toInt_umod` lemmas, but
instead choose to provide more specialized rewrites, with extra
side-conditions.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
This PR adds a `toFin` and `msb` lemma for unsigned bitvector division.
We *don't* have `toInt_udiv`, since the only truly general statement we
can make does no better than unfolding the definition, and it's not
uncontroversially clear how to unfold `toInt` (see
`toInt_eq_msb_cond`/`toInt_eq_toNat_cond`/`toInt_eq_toNat_bmod` for a
few options currently provided). Instead, we do have `toInt_udiv_of_msb`
that's able to provide a more meaningful rewrite given an extra
side-condition (that `x.msb = false`).
This PR also upstreams a minor `Nat` theorem (`Nat.div_le_div_left`)
needed for the above from Mathlib.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
This PR adds `BitVec.[toFin|getMsbD]_setWidth` and
`[getMsb|msb]_signExtend` as well as `ofInt_toInt`.
Also correct renamed the misnamed theorem for
`signExtend_eq_setWidth_of_msb_false`.
---------
Co-authored-by: Siddharth <siddu.druid@gmail.com>
This PR adds `protected` to `Fin.cast` and `BitVec.cast`, to avoid
confusion with `_root_.cast`. These should mostly be used via
dot-notation in any case.
This PR adds `BitVec.[toInt|toFin]_concat` and moves a couple of
theorems into the concat section, as `BitVec.msb_concat` is needed for
the `toInt_concat` proof.
We also add `Bool.toInt`.
This PR adds theorems characterizing the value of the unsigned shift
right of a bitvector in terms of its 2s complement interpretation as an
integer.
Unsigned shift right by at least one bit makes the value of the
bitvector less than or equal to `2^(w-1)`,
makes the interpretation of the bitvector `Int` and `Nat` agree.
In the case when `n = 0`, then the shift right value equals the integer
interpretation.
```lean
theorem toInt_ushiftRight_eq_ite {x : BitVec w} {n : Nat} :
(x >>> n).toInt = if n = 0 then x.toInt else x.toNat >>> n
```
```lean
theorem toFin_uShiftRight {x : BitVec w} {n : Nat} :
(x >>> n).toFin = x.toFin / (Fin.ofNat' (2^w) (2^n))
```
---------
Co-authored-by: Harun Khan <harun19@stanford.edu>
Co-authored-by: Tobias Grosser <github@grosser.es>
This PR implements `BitVec.toInt_abs`.
The absolute value of `x : BitVec w` is naively a case split on the sign
of `x`.
However, recall that when `x = intMin w`, `-x = x`.
Thus, the full value of `abs x` is computed by the case split:
- If `x : BitVec w` is `intMin`, then its absolute value is also `intMin
w`, and
thus `toInt` will equal `intMin.toInt`.
- Otherwise, if `x` is negative, then `x.abs.toInt = (-x).toInt`.
- Finally, when `x` is nonnegative, then `x.abs.toInt = x.toInt`.
```lean
theorem toInt_abs {x : BitVec w} :
x.abs.toInt =
if x = intMin w then (intMin w).toInt
else if x.msb then -x.toInt
else x.toInt
```
We also provide a variant of `toInt_abs` that
hides the case split for `x` being positive or negative by using
`natAbs`.
```lean
theorem toInt_abs_eq_natAbs {x : BitVec w} : x.abs.toInt =
if x = intMin w then (intMin w).toInt else x.toInt.natAbs
```
Supercedes https://github.com/leanprover/lean4/pull/5787
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
This PR adds `toNat` theorems for `BitVec.signExtend.`
Sign extending to a larger bitwidth depends on the msb. If the msb is
false, then the result equals the original value. If the msb is true,
then we add a value of `(2^v - 2^w)`, which arises from the sign
extension.
```lean
theorem toNat_signExtend (x : BitVec w) {v : Nat} :
(x.signExtend v).toNat = (x.setWidth v).toNat + if x.msb then 2^v - 2^w else 0
```
Co-authored-by: Harun Khan <harun19@stanford.edu>
This PR adds theorem `mod_eq_sub`, makes theorem
`sub_mul_eq_mod_of_lt_of_le` not private anymore and moves its location
within the `rotate*` section to use it in other proofs.
This PR adds toInt theorems for BitVec.signExtend.
If the current width `w` is larger than the extended width `v`,
then the value when interpreted as an integer is truncated,
and we compute a modulo by `2^v`.
```lean
theorem toInt_signExtend_of_le (x : BitVec w) (hv : v ≤ w) :
(x.signExtend v).toInt = Int.bmod (x.toNat) (2^v)
```
Co-authored-by: Siddharth Bhat <siddu.druid@gmail.com>
Co-authored-by: Harun Khan <harun19@stanford.edu>
Stacked on top of #6155
---------
Co-authored-by: Harun Khan <harun19@stanford.edu>
This PR adds lemmas for extracting a given bit of a `BitVec` obtained
via `sub`/`neg`/`sshiftRight'`/`abs`.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
This PR adds theorems `BitVec.(getMsbD, msb)_(rotateLeft, rotateRight)`.
We follow the same strategy taken for `getLsbD`, constructing the
necessary auxilliary theorems first (relying on different hypotheses)
and then generalizing.
---------
Co-authored-by: Siddharth <siddu.druid@gmail.com>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
This PR changes the signature of `Array.get` to take a Nat and a proof,
rather than a `Fin`, for consistency with the rest of the (planned)
Array API. Note that because of bootstrapping issues we can't provide
`get_elem_tactic` as an autoparameter for the proof. As users will
mostly use the `xs[i]` notation provided by `GetElem`, this hopefully
isn't a problem.
We may restore `Fin` based versions, either here or downstream, as
needed, but they won't be the "main" functions.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
This PR adds a normalization rule to `bv_normalize` (which is used by
`bv_decide`) that converts `x / 2^k` into `x >>> k` under suitable
conditions. This allows us to simplify the expensive division circuits
that are used for bitblasting into much cheaper shifting circuits.
Concretely, it allows for the following canonicalization:
```lean
example {x : BitVec 16} : x / (BitVec.twoPow 16 2) = x >>> 2 := by bv_normalize
example {x : BitVec 16} : x / (BitVec.ofNat 16 8) = x >>> 3 := by bv_normalize
```
This PR is a follow-up to https://github.com/leanprover/lean4/pull/5609,
where we add lemmas characterizing `smtUDiv` and `smtSDiv`'s behavior
when the denominator is zero.
We build some `slt` theory, connecting it to `msb` for a clean proof. I
chose not to characterize `slt` in terms of `msb` a `simp` lemma, since
I anticipate use cases where we want to keep the arithmetic
interpretation of `slt`.
