feat: getLsb_signExtend

[bollu]

The key idea is to notice that signExtend behavior is controlled by the msb. When msb = false, sext behaves the same as trunc. When msb = true, sext behaves like trunc but adds high 1-bits. This is expressed using the negate-truncate-negate pattern. Lemma statements below:

theorem signExtend_eq_neg_truncate_neg_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
    (x.signExtend v) = x.truncate v := by
 
theorem signExtend_eq_neg_truncate_neg_of_msb_true {x : BitVec w} {v : Nat} (hmsb : x.msb = true) :
    (x.signExtend v) = ~~~((~~~x).truncate v) := by

These give the final theorem statement:

theorem getLsb_signExtend {x  : BitVec w} {v i : Nat} :
    (x.signExtend v).getLsb i = (decide (i < v) && if i < w then x.getLsb i else x.msb) := by

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-06-02 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-06-02 18:15:31)

[bollu]

awaiting-review

[kim-em]

Close now!

[bollu]

awaiting-review

[tobiasgrosser]

@bollu, can you update the commit message accordingly.