max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: BitVec.extract_Lsb'_append_[ite|of_lt|of_le] (#7482)

Browse source 
This PR implements the
[BV_EXTRACT_CONCAT](6a1a768987/src/rewrite/rewrites_bv.cpp (L1264))
rule from Bitwuzla, which explains how to extract bits from an append.
We first prove a 'master theorem' which has the full case analysis, from
which we rapidly derive the necessary `BV_EXTRACT_CONCAT` theorems:

```lean
theorem extractLsb'_append_eq_ite {v w} {xhi : BitVec v} {xlo : BitVec w} {start len : Nat} :
    extractLsb' start len (xhi ++ xlo) =
    if hstart : start < w
    then
      if hlen : start + len < w
      then extractLsb' start len xlo
      else
        (((extractLsb' (start - w) (len - (w - start)) xhi) ++
            extractLsb' start (w - start) xlo)).cast (by omega)
    else
      extractLsb' (start - w) len xhi

theorem extractLsb'_append_eq_of_lt {v w} {xhi : BitVec v} {xlo : BitVec w}
    {start len : Nat} (h : start + len < w) :
    extractLsb' start len (xhi ++ xlo) = extractLsb' start len xlo

theorem extractLsb'_append_eq_of_le {v w} {xhi : BitVec v} {xlo : BitVec w}
    {start len : Nat} (h : w ≤ start) :
    extractLsb' start len (xhi ++ xlo) = extractLsb' (start - w) len xhi
```

---------

Co-authored-by: Tobias Grosser <github@grosser.es>
This commit is contained in:
Siddharth 2025-03-14 18:25:50 +00:00 • committed by GitHub
parent b55a5b0826
commit 1bbd2c183b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 66 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

66
src/Init/Data/BitVec/Lemmas.lean
View file

@ -2581,6 +2581,72 @@ theorem signExtend_eq_append_of_le {w v : Nat} {x : BitVec w} (h : w ≤ v) :
cases hx : x.msb <;>
simp [getElem_cast, hx, getElem_append, getElem_signExtend]
/--
The 'master theorem' for extracting bits from `(xhi ++ xlo)`,
which performs a case analysis on the start index, length, and the lengths of `xlo, xhi`.
· If the start index is entirely out of the `xlo` bitvector, then grab the bits from `xhi`.
· If the start index is entirely contained in the `xlo` bitvector, then grab the bits from `xlo`.
· If the start index is split between the two bitvectors,
then append `(w - start)` bits from `xlo` with `(len - (w - start))` bits from xhi.
Diagramatically:
```
xhi xlo
(<---------------------](<-------w--------]
start+len..start: (<-----len---*------]
w - start: *------*
len - (w -start): *------------*
```
-/
theorem extractLsb'_append_eq_ite {v w} {xhi : BitVec v} {xlo : BitVec w} {start len : Nat} :
extractLsb' start len (xhi ++ xlo) =
if hstart : start < w
then
if hlen : start + len < w
then extractLsb' start len xlo
else
(((extractLsb' (start - w) (len - (w - start)) xhi) ++
extractLsb' start (w - start) xlo)).cast (by omega)
else
extractLsb' (start - w) len xhi := by
by_cases hstart : start < w
· simp only [hstart, ↓reduceDIte]
by_cases hlen : start + len < w
· simp only [hlen, ↓reduceDIte]
ext i hi
simp only [getElem_extractLsb', getLsbD_append, ite_eq_left_iff, Nat.not_lt]
intros hcontra
omega
· simp only [hlen, ↓reduceDIte]
ext i hi
simp only [getElem_extractLsb', getLsbD_append, getElem_cast,
getElem_append, dite_eq_ite]
by_cases hi₂ : start + i < w
· simp [hi₂, show i < min len w by omega, show i < w - start by omega]
· simp [hi₂, ↓reduceIte, show ¬i < w - start by omega,
show start + i - w = start - w + (i - (w - start)) by omega]
· simp only [hstart, ↓reduceDIte]
ext i hi
simp [getElem_extractLsb', getLsbD_append,
show ¬start + i < w by omega, ↓reduceIte,
show start + i - w = start - w + i by omega]
/-- Extracting bits `[start..start+len)` from `(xhi ++ xlo)` equals extracting
the bits from `xlo` when `start + len` is within `xlo`.
-/
theorem extractLsb'_append_eq_of_lt {v w} {xhi : BitVec v} {xlo : BitVec w}
{start len : Nat} (h : start + len < w) :
extractLsb' start len (xhi ++ xlo) = extractLsb' start len xlo := by
simp [extractLsb'_append_eq_ite, h]
omega
/-- Extracting bits `[start..start+len)` from `(xhi ++ xlo)` equals extracting
the bits from `xhi` when `start` is outside `xlo`.
-/
theorem extractLsb'_append_eq_of_le {v w} {xhi : BitVec v} {xlo : BitVec w}
{start len : Nat} (h : w ≤ start) :
extractLsb' start len (xhi ++ xlo) = extractLsb' (start - w) len xhi := by
simp [extractLsb'_append_eq_ite, h, show ¬ start < w by omega]
/-! ### rev -/
theorem getLsbD_rev (x : BitVec w) (i : Fin w) :