Tobias Grosser
313f6b3c74
chore: name variables in Data/BitVec consistently ( #4930 )
...
This change canonicalizes the BitVec variable names to `x y z : BitVec`
instead of alternative namings such as `s t : BitVec` or `a b : BitVec`.
Variable names that carry semantic meaning such as `(msbs : BitVec w)
(lsb : Bool)` remain untouched.
This is purely a naming change to make our bitvector proofs more
consistent and polish the (auto-generated) documentation as a very small
step towards polishing the documentation of the BitVec library in Lean.
---------
Co-authored-by: AnotherAlexHere <153999274+AnotherAlexHere@users.noreply.github.com>
2024-08-07 13:43:15 +00:00
Siddharth
e106be19dd
feat: sshiftRight bitblasting ( #4889 )
...
We follow the same strategy as
https://github.com/leanprover/lean4/pull/4872 ,
https://github.com/leanprover/lean4/pull/4571 , and implement bitblasting
theorems for `sshiftRight`.
---------
Co-authored-by: Tobias Grosser <tobias@grosser.es>
2024-08-07 10:33:56 +00:00
Kim Morrison
c0ffc85d75
chore: require docs in BitVec ( #4913 )
2024-08-05 01:12:04 +00:00
Siddharth
c517688f1d
feat: ushiftRight bitblasting ( #4872 )
...
This adds theorems `ushiftRight_rec_zero`, `ushiftRight_rec_succ`,
`ushiftRight_rec_eq`, and `shiftRight_eq_shiftRight_rec`.
---------
Co-authored-by: Tobias Grosser <github@grosser.es>
2024-07-31 21:44:06 +00:00
Siddharth
bb9c9bd99f
feat: bitVec shiftLeft recurrences for bitblasting ( #4571 )
...
```lean
@[simp]
theorem shiftLeftRec_zero (x : BitVec w₁) (y : BitVec w₂) :
shiftLeftRec x y 0 = x <<< (y &&& twoPow w₂ 0) := by
simp [shiftLeftRec]
@[simp]
theorem shiftLeftRec_succ (x : BitVec w₁) (y : BitVec w₂) :
shiftLeftRec x y (n + 1) =
(shiftLeftRec x y n) <<< (y &&& twoPow w₂ (n + 1)) := by
simp [shiftLeftRec]
theorem shiftLeftRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) (hn : n + 1 ≤ w₂) :
shiftLeftRec x y n = x <<< (y.truncate (n + 1)).zeroExtend w₂ := by
```
These theorems are used for bitblasting shiftLeft in LeanSAT.
---------
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Kim Morrison <scott@tqft.net>
Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
2024-07-27 06:36:52 +00:00
Siddharth
e9d2f8f5f2
feat: mul recurrence theorems for LeanSAT ( #4568 )
...
This implements the recurrence theorems `getLsb_mul`, `mulRec_zero_eq`,
`mulRec_succ_eq` to allow bitblasting multiplication.
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
2024-07-01 23:47:29 +00:00
Alex Keizer
4fa3b3c4a0
feat: bitblasting theorems for signed comparisons ( #4201 )
...
Prove theorems that relate `BitVec.slt` and `sle` to `carry`, so that
these signed comparisons may be bitblasted in LeanSAT.
This PR is stacked on top of #4200 . For the diff without changes from
that PR, see:
https://github.com/opencompl/lean4/compare/opencompl:lean4:bitvec-toInt-iff-msb...bitvec-slt-blast
---------
Co-authored-by: Kim Morrison <scott@tqft.net>
2024-05-23 01:24:04 +00:00
Alex Keizer
2a966b46f2
feat: bitblasting theorems about unsigned bitvector inequalities ( #4178 )
...
This PR adds theorems that relate unsigned bitvector comparisons
`BitVec.ult` and `BitVec.ule` to `BitVec.carry`. These lemmas are a
prerequisite to bit-blasting these comparisons in LeanSAT.
2024-05-16 00:01:31 +00:00
Harun Khan
b1bedbe0d2
feat: equivalence of bit-vector negation and bitblasted negation ( #3920 )
2024-05-06 06:03:28 +00:00
Scott Morrison
ae492265fe
chore: cleanup a bitblast proof ( #3598 )
2024-03-05 04:59:58 +00:00
Leonardo de Moura
4d4b79757d
chore: move BitVec to top level namespace
...
Motivation: `Nat`, `Int`, `Fin`, `UInt??` are already in the top level
namespace. We will eventually define `UInt??` and `Int??` using `BitVec`.
2024-02-23 15:15:57 -08:00
Scott Morrison
4e87d7f173
chore: rename Bool.toNat_le_one ( #3469 )
...
To merge after #3457 .
---------
Co-authored-by: Alex Keizer <alex@keizer.dev>
2024-02-23 02:07:18 +00:00
Scott Morrison
7f7d9bdaaf
chore: cleanup in BitVec/Bitblast.lean ( #3468 )
2024-02-23 00:47:30 +00:00
Alex Keizer
815200eaad
refactor: make BitVec.carry take bitvector arguments ( #3461 )
...
Every usage of `carry` followed the pattern: `carry _ x.toNat y.toNat`,
so we've refactorod `carry` to take the `BitVec`s as arguments, and made
the `toNat` part of its definition.
2024-02-22 19:25:01 +00:00
Joe Hendrix
61c22c88d7
chore: address copyright inconsistencies ( #3448 )
2024-02-22 06:23:50 -08:00
Scott Morrison
ca941249b9
chore: upstream Std.BitVec.* ( #3400 )
...
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
2024-02-19 12:43:34 -08:00
