feat: proposed change to BitVec API (#5200)
This renames `BitVec.getLsb` to `getLsbD` (`D` for "default" value, i.e.
false), and introduces `getLsb?` and `getLsb'` (which we can rename to
`getLsb` after a deprecation cycle).
(Similarly for `getMsb`.)
Also adds a `GetElem` class so we can use `x[i]` and `x[i]?` notation.
Later, we will turn
```
theorem getLsbD_eq_getElem?_getD (x : BitVec w) (i : Nat) (h : i < w) :
x.getLsbD i = x[i]?.getD false
```
on as a `@[simp]` lemma.
This PR doesn't attempt to demonstrate the benefits, but I think both
arguments are going to get easier, and this will bring the BitVec API
closer in line to List/Array, etc.
---------
Co-authored-by: Markus Himmel <markus@lean-fro.org>
This commit is contained in:
Kim Morrison
GitHub
parent
f30ff6ae79
commit
6b62fed82e
35 changed files with 638 additions and 501 deletions
|
|
@ -116,17 +116,62 @@ end zero_allOnes
|
|||
|
||||
section getXsb
|
||||
|
||||
/--
|
||||
Return the `i`-th least significant bit.
|
||||
|
||||
This will be renamed `getLsb` after the existing deprecated alias is removed.
|
||||
-/
|
||||
@[inline] def getLsb' (x : BitVec w) (i : Fin w) : Bool := x.toNat.testBit i
|
||||
|
||||
/-- Return the `i`-th least significant bit or `none` if `i ≥ w`. -/
|
||||
@[inline] def getLsb? (x : BitVec w) (i : Nat) : Option Bool :=
|
||||
if h : i < w then some (getLsb' x ⟨i, h⟩) else none
|
||||
|
||||
/--
|
||||
Return the `i`-th most significant bit.
|
||||
|
||||
This will be renamed `getMsb` after the existing deprecated alias is removed.
|
||||
-/
|
||||
@[inline] def getMsb' (x : BitVec w) (i : Fin w) : Bool := x.getLsb' ⟨w-1-i, by omega⟩
|
||||
|
||||
/-- Return the `i`-th most significant bit or `none` if `i ≥ w`. -/
|
||||
@[inline] def getMsb? (x : BitVec w) (i : Nat) : Option Bool :=
|
||||
if h : i < w then some (getMsb' x ⟨i, h⟩) else none
|
||||
|
||||
/-- Return the `i`-th least significant bit or `false` if `i ≥ w`. -/
|
||||
@[inline] def getLsb (x : BitVec w) (i : Nat) : Bool := x.toNat.testBit i
|
||||
@[inline] def getLsbD (x : BitVec w) (i : Nat) : Bool :=
|
||||
x.toNat.testBit i
|
||||
|
||||
@[deprecated getLsbD (since := "2024-08-29"), inherit_doc getLsbD]
|
||||
def getLsb (x : BitVec w) (i : Nat) : Bool := x.getLsbD i
|
||||
|
||||
/-- Return the `i`-th most significant bit or `false` if `i ≥ w`. -/
|
||||
@[inline] def getMsb (x : BitVec w) (i : Nat) : Bool := i < w && getLsb x (w-1-i)
|
||||
@[inline] def getMsbD (x : BitVec w) (i : Nat) : Bool :=
|
||||
i < w && x.getLsbD (w-1-i)
|
||||
|
||||
@[deprecated getMsbD (since := "2024-08-29"), inherit_doc getMsbD]
|
||||
def getMsb (x : BitVec w) (i : Nat) : Bool := x.getMsbD i
|
||||
|
||||
/-- Return most-significant bit in bitvector. -/
|
||||
@[inline] protected def msb (x : BitVec n) : Bool := getMsb x 0
|
||||
@[inline] protected def msb (x : BitVec n) : Bool := getMsbD x 0
|
||||
|
||||
end getXsb
|
||||
|
||||
section getElem
|
||||
|
||||
instance : GetElem (BitVec w) Nat Bool fun _ i => i < w where
|
||||
getElem xs i h := xs.getLsb' ⟨i, h⟩
|
||||
|
||||
/-- We prefer `x[i]` as the simp normal form for `getLsb'` -/
|
||||
@[simp] theorem getLsb'_eq_getElem (x : BitVec w) (i : Fin w) :
|
||||
x.getLsb' i = x[i] := rfl
|
||||
|
||||
/-- We prefer `x[i]?` as the simp normal form for `getLsb?` -/
|
||||
@[simp] theorem getLsb?_eq_getElem? (x : BitVec w) (i : Nat) :
|
||||
x.getLsb? i = x[i]? := rfl
|
||||
|
||||
end getElem
|
||||
|
||||
section Int
|
||||
|
||||
/-- Interpret the bitvector as an integer stored in two's complement form. -/
|
||||
|
|
|
|||
|
|
@ -92,8 +92,8 @@ def carry (i : Nat) (x y : BitVec w) (c : Bool) : Bool :=
|
|||
cases c <;> simp [carry, mod_one]
|
||||
|
||||
theorem carry_succ (i : Nat) (x y : BitVec w) (c : Bool) :
|
||||
carry (i+1) x y c = atLeastTwo (x.getLsb i) (y.getLsb i) (carry i x y c) := by
|
||||
simp only [carry, mod_two_pow_succ, atLeastTwo, getLsb]
|
||||
carry (i+1) x y c = atLeastTwo (x.getLsbD i) (y.getLsbD i) (carry i x y c) := by
|
||||
simp only [carry, mod_two_pow_succ, atLeastTwo, getLsbD]
|
||||
simp only [Nat.pow_succ']
|
||||
have sum_bnd : x.toNat%2^i + (y.toNat%2^i + c.toNat) < 2*2^i := by
|
||||
simp only [← Nat.pow_succ']
|
||||
|
|
@ -110,7 +110,7 @@ theorem carry_of_and_eq_zero {x y : BitVec w} (h : x &&& y = 0#w) : carry i x y
|
|||
induction i with
|
||||
| zero => simp
|
||||
| succ i ih =>
|
||||
replace h := congrArg (·.getLsb i) h
|
||||
replace h := congrArg (·.getLsbD i) h
|
||||
simp_all [carry_succ]
|
||||
|
||||
/-- The final carry bit when computing `x + y + c` is `true` iff `x.toNat + y.toNat + c.toNat ≥ 2^w`. -/
|
||||
|
|
@ -136,14 +136,14 @@ def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, Bool.xor x (Bool.xo
|
|||
|
||||
/-- Bitwise addition implemented via a ripple carry adder. -/
|
||||
def adc (x y : BitVec w) : Bool → Bool × BitVec w :=
|
||||
iunfoldr fun (i : Fin w) c => adcb (x.getLsb i) (y.getLsb i) c
|
||||
iunfoldr fun (i : Fin w) c => adcb (x.getLsbD i) (y.getLsbD i) c
|
||||
|
||||
theorem getLsb_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
|
||||
getLsb (x + y + zeroExtend w (ofBool c)) i =
|
||||
Bool.xor (getLsb x i) (Bool.xor (getLsb y i) (carry i x y c)) := by
|
||||
theorem getLsbD_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
|
||||
getLsbD (x + y + zeroExtend w (ofBool c)) i =
|
||||
Bool.xor (getLsbD x i) (Bool.xor (getLsbD y i) (carry i x y c)) := by
|
||||
let ⟨x, x_lt⟩ := x
|
||||
let ⟨y, y_lt⟩ := y
|
||||
simp only [getLsb, toNat_add, toNat_zeroExtend, i_lt, toNat_ofFin, toNat_ofBool,
|
||||
simp only [getLsbD, toNat_add, toNat_zeroExtend, i_lt, toNat_ofFin, toNat_ofBool,
|
||||
Nat.mod_add_mod, Nat.add_mod_mod]
|
||||
apply Eq.trans
|
||||
rw [← Nat.div_add_mod x (2^i), ← Nat.div_add_mod y (2^i)]
|
||||
|
|
@ -159,10 +159,10 @@ theorem getLsb_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool)
|
|||
]
|
||||
simp [testBit_to_div_mod, carry, Nat.add_assoc]
|
||||
|
||||
theorem getLsb_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
|
||||
getLsb (x + y) i =
|
||||
Bool.xor (getLsb x i) (Bool.xor (getLsb y i) (carry i x y false)) := by
|
||||
simpa using getLsb_add_add_bool i_lt x y false
|
||||
theorem getLsbD_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
|
||||
getLsbD (x + y) i =
|
||||
Bool.xor (getLsbD x i) (Bool.xor (getLsbD y i) (carry i x y false)) := by
|
||||
simpa using getLsbD_add_add_bool i_lt x y false
|
||||
|
||||
theorem adc_spec (x y : BitVec w) (c : Bool) :
|
||||
adc x y c = (carry w x y c, x + y + zeroExtend w (ofBool c)) := by
|
||||
|
|
@ -175,7 +175,7 @@ theorem adc_spec (x y : BitVec w) (c : Bool) :
|
|||
simp [carry, Nat.mod_one]
|
||||
cases c <;> rfl
|
||||
case step =>
|
||||
simp [adcb, Prod.mk.injEq, carry_succ, getLsb_add_add_bool]
|
||||
simp [adcb, Prod.mk.injEq, carry_succ, getLsbD_add_add_bool]
|
||||
|
||||
theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := by
|
||||
simp [adc_spec]
|
||||
|
|
@ -197,37 +197,37 @@ theorem add_eq_or_of_and_eq_zero {w : Nat} (x y : BitVec w)
|
|||
(h : x &&& y = 0#w) : x + y = x ||| y := by
|
||||
rw [add_eq_adc, adc, iunfoldr_replace (fun _ => false) (x ||| y)]
|
||||
· rfl
|
||||
· simp only [adcb, atLeastTwo, Bool.and_false, Bool.or_false, bne_false, getLsb_or,
|
||||
· simp only [adcb, atLeastTwo, Bool.and_false, Bool.or_false, bne_false, getLsbD_or,
|
||||
Prod.mk.injEq, and_eq_false_imp]
|
||||
intros i
|
||||
replace h : (x &&& y).getLsb i = (0#w).getLsb i := by rw [h]
|
||||
simp only [getLsb_and, getLsb_zero, and_eq_false_imp] at h
|
||||
replace h : (x &&& y).getLsbD i = (0#w).getLsbD i := by rw [h]
|
||||
simp only [getLsbD_and, getLsbD_zero, and_eq_false_imp] at h
|
||||
constructor
|
||||
· intros hx
|
||||
simp_all [hx]
|
||||
· by_cases hx : x.getLsb i <;> simp_all [hx]
|
||||
· by_cases hx : x.getLsbD i <;> simp_all [hx]
|
||||
|
||||
/-! ### Negation -/
|
||||
|
||||
theorem bit_not_testBit (x : BitVec w) (i : Fin w) :
|
||||
getLsb (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) i.val = !(getLsb x i.val) := by
|
||||
apply iunfoldr_getLsb (fun _ => ()) i (by simp)
|
||||
getLsbD (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd) i.val = !(getLsbD x i.val) := by
|
||||
apply iunfoldr_getLsbD (fun _ => ()) i (by simp)
|
||||
|
||||
theorem bit_not_add_self (x : BitVec w) :
|
||||
((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd + x = -1 := by
|
||||
((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd + x = -1 := by
|
||||
simp only [add_eq_adc]
|
||||
apply iunfoldr_replace_snd (fun _ => false) (-1) false rfl
|
||||
intro i; simp only [ BitVec.not, adcb, testBit_toNat]
|
||||
rw [iunfoldr_replace_snd (fun _ => ()) (((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd)]
|
||||
<;> simp [bit_not_testBit, negOne_eq_allOnes, getLsb_allOnes]
|
||||
rw [iunfoldr_replace_snd (fun _ => ()) (((iunfoldr (fun i c => (c, !(x.getLsbD i)))) ()).snd)]
|
||||
<;> simp [bit_not_testBit, negOne_eq_allOnes, getLsbD_allOnes]
|
||||
|
||||
theorem bit_not_eq_not (x : BitVec w) :
|
||||
((iunfoldr (fun i c => (c, !(x.getLsb i)))) ()).snd = ~~~ x := by
|
||||
((iunfoldr (fun i c => (c, !(x.getLsbD i)))) ()).snd = ~~~ x := by
|
||||
simp [←allOnes_sub_eq_not, BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), ←negOne_eq_allOnes]
|
||||
|
||||
theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) (BitVec.ofNat w 1) false).snd:= by
|
||||
theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd) (BitVec.ofNat w 1) false).snd:= by
|
||||
simp only [← add_eq_adc]
|
||||
rw [iunfoldr_replace_snd ((fun _ => ())) (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsb i)))) ()).snd) _ rfl]
|
||||
rw [iunfoldr_replace_snd ((fun _ => ())) (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd) _ rfl]
|
||||
· rw [BitVec.eq_sub_iff_add_eq.mpr (bit_not_add_self x), sub_toAdd, BitVec.add_comm _ (-x)]
|
||||
simp [← sub_toAdd, BitVec.sub_add_cancel]
|
||||
· simp [bit_not_testBit x _]
|
||||
|
|
@ -290,17 +290,17 @@ A recurrence that describes multiplication as repeated addition.
|
|||
Is useful for bitblasting multiplication.
|
||||
-/
|
||||
def mulRec (x y : BitVec w) (s : Nat) : BitVec w :=
|
||||
let cur := if y.getLsb s then (x <<< s) else 0
|
||||
let cur := if y.getLsbD s then (x <<< s) else 0
|
||||
match s with
|
||||
| 0 => cur
|
||||
| s + 1 => mulRec x y s + cur
|
||||
|
||||
theorem mulRec_zero_eq (x y : BitVec w) :
|
||||
mulRec x y 0 = if y.getLsb 0 then x else 0 := by
|
||||
mulRec x y 0 = if y.getLsbD 0 then x else 0 := by
|
||||
simp [mulRec]
|
||||
|
||||
theorem mulRec_succ_eq (x y : BitVec w) (s : Nat) :
|
||||
mulRec x y (s + 1) = mulRec x y s + if y.getLsb (s + 1) then (x <<< (s + 1)) else 0 := rfl
|
||||
mulRec x y (s + 1) = mulRec x y s + if y.getLsbD (s + 1) then (x <<< (s + 1)) else 0 := rfl
|
||||
|
||||
/--
|
||||
Recurrence lemma: truncating to `i+1` bits and then zero extending to `w`
|
||||
|
|
@ -311,11 +311,11 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w
|
|||
zeroExtend w (x.truncate i) + (x &&& twoPow w i) := by
|
||||
rw [add_eq_or_of_and_eq_zero]
|
||||
· ext k
|
||||
simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsb_or, getLsb_and]
|
||||
simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
|
||||
by_cases hik : i = k
|
||||
· subst hik
|
||||
simp
|
||||
· simp only [getLsb_twoPow, hik, decide_False, Bool.and_false, Bool.or_false]
|
||||
· simp only [getLsbD_twoPow, hik, decide_False, Bool.and_false, Bool.or_false]
|
||||
by_cases hik' : k < (i + 1)
|
||||
· have hik'' : k < i := by omega
|
||||
simp [hik', hik'']
|
||||
|
|
@ -323,7 +323,7 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w
|
|||
simp [hik', hik'']
|
||||
· ext k
|
||||
simp
|
||||
by_cases hi : x.getLsb i <;> simp [hi] <;> omega
|
||||
by_cases hi : x.getLsbD i <;> simp [hi] <;> omega
|
||||
|
||||
/--
|
||||
Recurrence lemma: multiplying `x` with the first `s` bits of `y` is the
|
||||
|
|
@ -334,7 +334,7 @@ theorem mulRec_eq_mul_signExtend_truncate (x y : BitVec w) (s : Nat) :
|
|||
induction s
|
||||
case zero =>
|
||||
simp only [mulRec_zero_eq, ofNat_eq_ofNat, Nat.reduceAdd]
|
||||
by_cases y.getLsb 0
|
||||
by_cases y.getLsbD 0
|
||||
case pos hy =>
|
||||
simp only [hy, ↓reduceIte, truncate, zeroExtend_one_eq_ofBool_getLsb_zero,
|
||||
ofBool_true, ofNat_eq_ofNat]
|
||||
|
|
@ -345,14 +345,14 @@ theorem mulRec_eq_mul_signExtend_truncate (x y : BitVec w) (s : Nat) :
|
|||
case succ s' hs =>
|
||||
rw [mulRec_succ_eq, hs]
|
||||
have heq :
|
||||
(if y.getLsb (s' + 1) = true then x <<< (s' + 1) else 0) =
|
||||
(if y.getLsbD (s' + 1) = true then x <<< (s' + 1) else 0) =
|
||||
(x * (y &&& (BitVec.twoPow w (s' + 1)))) := by
|
||||
simp only [ofNat_eq_ofNat, and_twoPow]
|
||||
by_cases hy : y.getLsb (s' + 1) <;> simp [hy]
|
||||
by_cases hy : y.getLsbD (s' + 1) <;> simp [hy]
|
||||
rw [heq, ← BitVec.mul_add, ← zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow]
|
||||
|
||||
theorem getLsb_mul (x y : BitVec w) (i : Nat) :
|
||||
(x * y).getLsb i = (mulRec x y w).getLsb i := by
|
||||
theorem getLsbD_mul (x y : BitVec w) (i : Nat) :
|
||||
(x * y).getLsbD i = (mulRec x y w).getLsbD i := by
|
||||
simp only [mulRec_eq_mul_signExtend_truncate]
|
||||
rw [truncate, ← truncate_eq_zeroExtend, ← truncate_eq_zeroExtend,
|
||||
truncate_truncate_of_le]
|
||||
|
|
@ -406,17 +406,17 @@ theorem shiftLeftRec_eq {x : BitVec w₁} {y : BitVec w₂} {n : Nat} :
|
|||
case zero =>
|
||||
ext i
|
||||
simp only [shiftLeftRec_zero, twoPow_zero, Nat.reduceAdd, truncate_one,
|
||||
and_one_eq_zeroExtend_ofBool_getLsb]
|
||||
and_one_eq_zeroExtend_ofBool_getLsbD]
|
||||
case succ n ih =>
|
||||
simp only [shiftLeftRec_succ, and_twoPow]
|
||||
rw [ih]
|
||||
by_cases h : y.getLsb (n + 1)
|
||||
by_cases h : y.getLsbD (n + 1)
|
||||
· simp only [h, ↓reduceIte]
|
||||
rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true h,
|
||||
rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
|
||||
shiftLeft_or_of_and_eq_zero]
|
||||
simp
|
||||
· simp only [h, false_eq_true, ↓reduceIte, shiftLeft_zero']
|
||||
rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false (i := n + 1)]
|
||||
rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false (i := n + 1)]
|
||||
simp [h]
|
||||
|
||||
/--
|
||||
|
|
@ -469,14 +469,14 @@ theorem sshiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
|
|||
induction n generalizing x y
|
||||
case zero =>
|
||||
ext i
|
||||
simp [twoPow_zero, Nat.reduceAdd, and_one_eq_zeroExtend_ofBool_getLsb, truncate_one]
|
||||
simp [twoPow_zero, Nat.reduceAdd, and_one_eq_zeroExtend_ofBool_getLsbD, truncate_one]
|
||||
case succ n ih =>
|
||||
simp only [sshiftRightRec_succ_eq, and_twoPow, ih]
|
||||
by_cases h : y.getLsb (n + 1)
|
||||
· rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true h,
|
||||
by_cases h : y.getLsbD (n + 1)
|
||||
· rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
|
||||
sshiftRight'_or_of_and_eq_zero (by simp), h]
|
||||
simp
|
||||
· rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false (i := n + 1)
|
||||
· rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false (i := n + 1)
|
||||
(by simp [h])]
|
||||
simp [h]
|
||||
|
||||
|
|
@ -485,7 +485,7 @@ Show that `x.sshiftRight y` can be written in terms of `sshiftRightRec`.
|
|||
This can be unfolded in terms of `sshiftRightRec_zero_eq`, `sshiftRightRec_succ_eq` for bitblasting.
|
||||
-/
|
||||
theorem sshiftRight_eq_sshiftRightRec (x : BitVec w₁) (y : BitVec w₂) :
|
||||
(x.sshiftRight' y).getLsb i = (sshiftRightRec x y (w₂ - 1)).getLsb i := by
|
||||
(x.sshiftRight' y).getLsbD i = (sshiftRightRec x y (w₂ - 1)).getLsbD i := by
|
||||
rcases w₂ with rfl | w₂
|
||||
· simp [of_length_zero]
|
||||
· simp [sshiftRightRec_eq]
|
||||
|
|
@ -533,15 +533,15 @@ theorem ushiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
|
|||
case zero =>
|
||||
ext i
|
||||
simp only [ushiftRightRec_zero, twoPow_zero, Nat.reduceAdd,
|
||||
and_one_eq_zeroExtend_ofBool_getLsb, truncate_one]
|
||||
and_one_eq_zeroExtend_ofBool_getLsbD, truncate_one]
|
||||
case succ n ih =>
|
||||
simp only [ushiftRightRec_succ, and_twoPow]
|
||||
rw [ih]
|
||||
by_cases h : y.getLsb (n + 1) <;> simp only [h, ↓reduceIte]
|
||||
· rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true h,
|
||||
by_cases h : y.getLsbD (n + 1) <;> simp only [h, ↓reduceIte]
|
||||
· rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
|
||||
ushiftRight'_or_of_and_eq_zero]
|
||||
simp
|
||||
· simp [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false, h]
|
||||
· simp [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false, h]
|
||||
|
||||
/--
|
||||
Show that `x >>> y` can be written in terms of `ushiftRightRec`.
|
||||
|
|
|
|||
|
|
@ -41,7 +41,7 @@ theorem iunfoldr.fst_eq
|
|||
private theorem iunfoldr.eq_test
|
||||
{f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
|
||||
(init : state 0 = a)
|
||||
(step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
|
||||
(step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsbD i.val)) :
|
||||
iunfoldr f a = (state w, BitVec.truncate w value) := by
|
||||
apply Fin.hIterate_eq (fun i => ((state i, BitVec.truncate i value) : α × BitVec i))
|
||||
case init =>
|
||||
|
|
@ -50,15 +50,15 @@ private theorem iunfoldr.eq_test
|
|||
intro i
|
||||
simp_all [truncate_succ]
|
||||
|
||||
theorem iunfoldr_getLsb' {f : Fin w → α → α × Bool} (state : Nat → α)
|
||||
theorem iunfoldr_getLsbD' {f : Fin w → α → α × Bool} (state : Nat → α)
|
||||
(ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
|
||||
(∀ i : Fin w, getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd)
|
||||
(∀ i : Fin w, getLsbD (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd)
|
||||
∧ (iunfoldr f (state 0)).fst = state w := by
|
||||
unfold iunfoldr
|
||||
simp
|
||||
apply Fin.hIterate_elim
|
||||
(fun j (p : α × BitVec j) => (hj : j ≤ w) →
|
||||
(∀ i : Fin j, getLsb p.snd i.val = (f ⟨i.val, Nat.lt_of_lt_of_le i.isLt hj⟩ (state i.val)).snd)
|
||||
(∀ i : Fin j, getLsbD p.snd i.val = (f ⟨i.val, Nat.lt_of_lt_of_le i.isLt hj⟩ (state i.val)).snd)
|
||||
∧ p.fst = state j)
|
||||
case hj => simp
|
||||
case init =>
|
||||
|
|
@ -73,7 +73,7 @@ theorem iunfoldr_getLsb' {f : Fin w → α → α × Bool} (state : Nat → α)
|
|||
apply And.intro
|
||||
case left =>
|
||||
intro i
|
||||
simp only [getLsb_cons]
|
||||
simp only [getLsbD_cons]
|
||||
have hj2 : j.val ≤ w := by simp
|
||||
cases (Nat.lt_or_eq_of_le (Nat.lt_succ.mp i.isLt)) with
|
||||
| inl h3 => simp [if_neg, (Nat.ne_of_lt h3)]
|
||||
|
|
@ -90,10 +90,10 @@ theorem iunfoldr_getLsb' {f : Fin w → α → α × Bool} (state : Nat → α)
|
|||
rw [← ind j, ← (ih hj2).2]
|
||||
|
||||
|
||||
theorem iunfoldr_getLsb {f : Fin w → α → α × Bool} (state : Nat → α) (i : Fin w)
|
||||
theorem iunfoldr_getLsbD {f : Fin w → α → α × Bool} (state : Nat → α) (i : Fin w)
|
||||
(ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
|
||||
getLsb (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd := by
|
||||
exact (iunfoldr_getLsb' state ind).1 i
|
||||
getLsbD (iunfoldr f (state 0)).snd i.val = (f i (state i.val)).snd := by
|
||||
exact (iunfoldr_getLsbD' state ind).1 i
|
||||
|
||||
/--
|
||||
Correctness theorem for `iunfoldr`.
|
||||
|
|
@ -101,14 +101,14 @@ Correctness theorem for `iunfoldr`.
|
|||
theorem iunfoldr_replace
|
||||
{f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
|
||||
(init : state 0 = a)
|
||||
(step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
|
||||
(step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsbD i.val)) :
|
||||
iunfoldr f a = (state w, value) := by
|
||||
simp [iunfoldr.eq_test state value a init step]
|
||||
|
||||
theorem iunfoldr_replace_snd
|
||||
{f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
|
||||
(init : state 0 = a)
|
||||
(step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
|
||||
(step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsbD i.val)) :
|
||||
(iunfoldr f a).snd = value := by
|
||||
simp [iunfoldr.eq_test state value a init step]
|
||||
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -255,7 +255,7 @@ theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l
|
|||
/-! ### getElem? and getElem -/
|
||||
|
||||
@[simp] theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] := by
|
||||
simp only [← get?_eq_getElem?, get?_eq_get, h, get_eq_getElem]
|
||||
simp only [getElem?_def, h, ↓reduceDIte]
|
||||
|
||||
theorem getElem?_eq_some {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length, l[n] = a := by
|
||||
simp only [← get?_eq_getElem?, get?_eq_some, get_eq_getElem]
|
||||
|
|
|
|||
|
|
@ -88,8 +88,8 @@ where
|
|||
go : BVPred → Expr
|
||||
| .bin (w := w) lhs op rhs =>
|
||||
mkApp4 (mkConst ``BVPred.bin) (toExpr w) (toExpr lhs) (toExpr op) (toExpr rhs)
|
||||
| .getLsb (w := w) expr idx =>
|
||||
mkApp3 (mkConst ``BVPred.getLsb) (toExpr w) (toExpr expr) (toExpr idx)
|
||||
| .getLsbD (w := w) expr idx =>
|
||||
mkApp3 (mkConst ``BVPred.getLsbD) (toExpr w) (toExpr expr) (toExpr idx)
|
||||
|
||||
|
||||
instance [ToExpr α] : ToExpr (BoolExpr α) where
|
||||
|
|
|
|||
|
|
@ -46,16 +46,16 @@ def of (t : Expr) : M (Option ReifiedBVPred) := do
|
|||
binaryReflection lhsExpr rhsExpr .eq ``Std.Tactic.BVDecide.Reflect.BitVec.beq_congr
|
||||
| BitVec.ult _ lhsExpr rhsExpr =>
|
||||
binaryReflection lhsExpr rhsExpr .ult ``Std.Tactic.BVDecide.Reflect.BitVec.ult_congr
|
||||
| BitVec.getLsb _ subExpr idxExpr =>
|
||||
| BitVec.getLsbD _ subExpr idxExpr =>
|
||||
let some sub ← ReifiedBVExpr.of subExpr | return none
|
||||
let some idx ← getNatValue? idxExpr | return none
|
||||
let bvExpr : BVPred := .getLsb sub.bvExpr idx
|
||||
let expr := mkApp3 (mkConst ``BVPred.getLsb) (toExpr sub.width) sub.expr idxExpr
|
||||
let bvExpr : BVPred := .getLsbD sub.bvExpr idx
|
||||
let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr
|
||||
let proof := do
|
||||
let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr
|
||||
let subProof ← sub.evalsAtAtoms
|
||||
return mkApp5
|
||||
(mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsb_congr)
|
||||
(mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr)
|
||||
idxExpr
|
||||
(toExpr sub.width)
|
||||
subExpr
|
||||
|
|
@ -73,8 +73,8 @@ def of (t : Expr) : M (Option ReifiedBVPred) := do
|
|||
let ty ← inferType t
|
||||
let_expr Bool := ty | return none
|
||||
let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1
|
||||
let bvExpr : BVPred := .getLsb atom.bvExpr 0
|
||||
let expr := mkApp3 (mkConst ``BVPred.getLsb) (toExpr 1) atom.expr (toExpr 0)
|
||||
let bvExpr : BVPred := .getLsbD atom.bvExpr 0
|
||||
let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0)
|
||||
let proof := do
|
||||
let atomEval ← ReifiedBVExpr.mkEvalExpr atom.width atom.expr
|
||||
let atomProof ← atom.evalsAtAtoms
|
||||
|
|
|
|||
|
|
@ -154,9 +154,9 @@ builtin_dsimproc [simp, seval] reduceSDiv ((sdiv _ _ : BitVec _)) := reduceBin `
|
|||
/-- Simplification procedure for signed division of `BitVec`s using the SMT-Lib conventions. -/
|
||||
builtin_dsimproc [simp, seval] reduceSMTSDiv ((smtSDiv _ _ : BitVec _)) := reduceBin ``smtSDiv 3 smtSDiv
|
||||
/-- Simplification procedure for `getLsb` (lowest significant bit) on `BitVec`. -/
|
||||
builtin_dsimproc [simp, seval] reduceGetLsb (getLsb _ _) := reduceGetBit ``getLsb getLsb
|
||||
builtin_dsimproc [simp, seval] reduceGetLsb (getLsbD _ _) := reduceGetBit ``getLsbD getLsbD
|
||||
/-- Simplification procedure for `getMsb` (most significant bit) on `BitVec`. -/
|
||||
builtin_dsimproc [simp, seval] reduceGetMsb (getMsb _ _) := reduceGetBit ``getMsb getMsb
|
||||
builtin_dsimproc [simp, seval] reduceGetMsb (getMsbD _ _) := reduceGetBit ``getMsbD getMsbD
|
||||
|
||||
/-- Simplification procedure for shift left on `BitVec`. -/
|
||||
builtin_dsimproc [simp, seval] reduceShiftLeft (BitVec.shiftLeft _ _) :=
|
||||
|
|
|
|||
|
|
@ -375,7 +375,7 @@ inductive BVPred where
|
|||
/--
|
||||
Getting a constant LSB from a `BitVec`.
|
||||
-/
|
||||
| getLsb (expr : BVExpr w) (idx : Nat)
|
||||
| getLsbD (expr : BVExpr w) (idx : Nat)
|
||||
|
||||
namespace BVPred
|
||||
|
||||
|
|
@ -389,7 +389,7 @@ structure ExprPair where
|
|||
|
||||
def toString : BVPred → String
|
||||
| bin lhs op rhs => s!"({lhs.toString} {op.toString} {rhs.toString})"
|
||||
| getLsb expr idx => s!"{expr.toString}[{idx}]"
|
||||
| getLsbD expr idx => s!"{expr.toString}[{idx}]"
|
||||
|
||||
instance : ToString BVPred := ⟨toString⟩
|
||||
|
||||
|
|
@ -398,14 +398,14 @@ The semantics for `BVPred`.
|
|||
-/
|
||||
def eval (assign : BVExpr.Assignment) : BVPred → Bool
|
||||
| bin lhs op rhs => op.eval (lhs.eval assign) (rhs.eval assign)
|
||||
| getLsb expr idx => (expr.eval assign).getLsb idx
|
||||
| getLsbD expr idx => (expr.eval assign).getLsbD idx
|
||||
|
||||
@[simp]
|
||||
theorem eval_bin : eval assign (.bin lhs op rhs) = op.eval (lhs.eval assign) (rhs.eval assign) := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
theorem eval_getLsb : eval assign (.getLsb expr idx) = (expr.eval assign).getLsb idx := by
|
||||
theorem eval_getLsbD : eval assign (.getLsbD expr idx) = (expr.eval assign).getLsbD idx := by
|
||||
rfl
|
||||
|
||||
end BVPred
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ where
|
|||
go (aig : AIG α) (val : BitVec w) (curr : Nat) (s : AIG.RefVec aig curr) (hcurr : curr ≤ w) :
|
||||
AIG.RefVecEntry α w :=
|
||||
if hcurr : curr < w then
|
||||
let res := aig.mkConstCached (val.getLsb curr)
|
||||
let res := aig.mkConstCached (val.getLsbD curr)
|
||||
let aig := res.aig
|
||||
let bitRef := res.ref
|
||||
let s := s.cast <| AIG.LawfulOperator.le_size (f := AIG.mkConstCached) ..
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
|
|||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Eq
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsb
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Not
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ import Std.Sat.AIG.CachedGatesLemmas
|
|||
import Std.Sat.AIG.RefVec
|
||||
|
||||
/-!
|
||||
This module contains the implementation of a bitblaster for `BitVec.getLsb`.
|
||||
This module contains the implementation of a bitblaster for `BitVec.getLsbD`.
|
||||
-/
|
||||
|
||||
namespace Std.Tactic.BVDecide
|
||||
|
|
@ -19,27 +19,27 @@ namespace BVPred
|
|||
|
||||
variable [Hashable α] [DecidableEq α]
|
||||
|
||||
structure GetLsbTarget (aig : AIG α) where
|
||||
structure GetLsbDTarget (aig : AIG α) where
|
||||
{w : Nat}
|
||||
vec : AIG.RefVec aig w
|
||||
idx : Nat
|
||||
|
||||
def blastGetLsb (aig : AIG α) (target : GetLsbTarget aig) : AIG.Entrypoint α :=
|
||||
def blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig) : AIG.Entrypoint α :=
|
||||
if h : target.idx < target.w then
|
||||
⟨aig, target.vec.get target.idx h⟩
|
||||
else
|
||||
AIG.mkConstCached aig false
|
||||
|
||||
instance : AIG.LawfulOperator α GetLsbTarget blastGetLsb where
|
||||
instance : AIG.LawfulOperator α GetLsbDTarget blastGetLsbD where
|
||||
le_size := by
|
||||
intros
|
||||
unfold blastGetLsb
|
||||
unfold blastGetLsbD
|
||||
split
|
||||
· simp
|
||||
· apply AIG.LawfulOperator.le_size (f := AIG.mkConstCached)
|
||||
decl_eq := by
|
||||
intros
|
||||
unfold blastGetLsb
|
||||
unfold blastGetLsbD
|
||||
split
|
||||
· simp
|
||||
· rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
|
||||
|
|
@ -6,7 +6,7 @@ Authors: Henrik Böving
|
|||
prelude
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Eq
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Ult
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsb
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
|
||||
|
||||
/-!
|
||||
|
|
@ -33,7 +33,7 @@ def bitblast (aig : AIG BVBit) (pred : BVPred) : AIG.Entrypoint BVBit :=
|
|||
match op with
|
||||
| .eq => mkEq aig ⟨lhsRefs, rhsRefs⟩
|
||||
| .ult => mkUlt aig ⟨lhsRefs, rhsRefs⟩
|
||||
| .getLsb expr idx =>
|
||||
| .getLsbD expr idx =>
|
||||
/-
|
||||
Note: This blasts the entire expression up to `w` despite only needing it up to `idx`.
|
||||
However the vast majority of operations are interested in all bits so the API is currently
|
||||
|
|
@ -42,7 +42,7 @@ def bitblast (aig : AIG BVBit) (pred : BVPred) : AIG.Entrypoint BVBit :=
|
|||
let res := expr.bitblast aig
|
||||
let aig := res.aig
|
||||
let refs := res.vec
|
||||
blastGetLsb aig ⟨refs, idx⟩
|
||||
blastGetLsbD aig ⟨refs, idx⟩
|
||||
|
||||
instance : AIG.LawfulOperator BVBit (fun _ => BVPred) bitblast where
|
||||
le_size := by
|
||||
|
|
@ -59,8 +59,8 @@ instance : AIG.LawfulOperator BVBit (fun _ => BVPred) bitblast where
|
|||
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
|
||||
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
|
||||
apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast)
|
||||
| getLsb expr idx =>
|
||||
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsb)
|
||||
| getLsbD expr idx =>
|
||||
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := blastGetLsbD)
|
||||
apply AIG.LawfulVecOperator.le_size (f := BVExpr.bitblast)
|
||||
decl_eq := by
|
||||
intro aig pred idx h1 h2
|
||||
|
|
@ -87,9 +87,9 @@ instance : AIG.LawfulOperator BVBit (fun _ => BVPred) bitblast where
|
|||
· apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
|
||||
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := BVExpr.bitblast)
|
||||
assumption
|
||||
| getLsb expr idx =>
|
||||
| getLsbD expr idx =>
|
||||
simp only [bitblast]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := blastGetLsb)]
|
||||
rw [AIG.LawfulOperator.decl_eq (f := blastGetLsbD)]
|
||||
rw [AIG.LawfulVecOperator.decl_eq (f := BVExpr.bitblast)]
|
||||
apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := BVExpr.bitblast)
|
||||
assumption
|
||||
|
|
|
|||
|
|
@ -18,11 +18,11 @@ namespace Std.Tactic.BVDecide
|
|||
namespace BVExpr
|
||||
|
||||
def Assignment.toAIGAssignment (assign : Assignment) : BVBit → Bool :=
|
||||
fun bit => (assign.getD bit.var).bv.getLsb bit.idx
|
||||
fun bit => (assign.getD bit.var).bv.getLsbD bit.idx
|
||||
|
||||
@[simp]
|
||||
theorem Assignment.toAIGAssignment_apply (assign : Assignment) (bit : BVBit) :
|
||||
assign.toAIGAssignment bit = (assign.getD bit.var).bv.getLsb bit.idx := by
|
||||
assign.toAIGAssignment bit = (assign.getD bit.var).bv.getLsbD bit.idx := by
|
||||
rfl
|
||||
|
||||
end BVExpr
|
||||
|
|
|
|||
|
|
@ -26,8 +26,8 @@ namespace mkOverflowBit
|
|||
|
||||
theorem go_eq_carry (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig) (origCin : Ref aig)
|
||||
(lhs rhs : RefVec aig w) (lhsExpr rhsExpr : BitVec w) (assign : α → Bool)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign⟧ = lhsExpr.getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign⟧ = rhsExpr.getLsb idx)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign⟧ = lhsExpr.getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign⟧ = rhsExpr.getLsbD idx)
|
||||
(hcin : ⟦aig, cin, assign⟧ = BitVec.carry curr lhsExpr rhsExpr ⟦aig, origCin, assign⟧) :
|
||||
⟦go aig lhs rhs curr hcurr cin, assign⟧
|
||||
=
|
||||
|
|
@ -59,8 +59,8 @@ end mkOverflowBit
|
|||
|
||||
theorem mkOverflowBit_eq_carry (aig : AIG α) (input : OverflowInput aig) (lhs rhs : BitVec input.w)
|
||||
(assign : α → Bool)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.vec.lhs.get idx hidx, assign⟧ = lhs.getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.vec.rhs.get idx hidx, assign⟧ = rhs.getLsb idx) :
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.vec.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.vec.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
|
||||
⟦mkOverflowBit aig input, assign⟧
|
||||
=
|
||||
BitVec.carry input.w lhs rhs ⟦aig, input.cin, assign⟧ := by
|
||||
|
|
|
|||
|
|
@ -87,7 +87,7 @@ theorem go_denote_eq (aig : AIG α) (c : BitVec w) (assign : α → Bool)
|
|||
assign
|
||||
⟧
|
||||
=
|
||||
c.getLsb idx := by
|
||||
c.getLsbD idx := by
|
||||
intro idx hidx1 hidx2
|
||||
generalize hgo : go aig c curr s hcurr = res
|
||||
unfold go at hgo
|
||||
|
|
@ -117,7 +117,7 @@ theorem denote_blastConst (aig : AIG α) (c : BitVec w) (assign : α → Bool) :
|
|||
∀ (idx : Nat) (hidx : idx < w),
|
||||
⟦(blastConst aig c).aig, (blastConst aig c).vec.get idx hidx, assign⟧
|
||||
=
|
||||
c.getLsb idx := by
|
||||
c.getLsbD idx := by
|
||||
intros
|
||||
apply blastConst.go_denote_eq
|
||||
omega
|
||||
|
|
|
|||
|
|
@ -58,7 +58,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
|
|||
∀ (idx : Nat) (hidx : idx < w),
|
||||
⟦(go aig expr).val.aig, (go aig expr).val.vec.get idx hidx, assign.toAIGAssignment⟧
|
||||
=
|
||||
(expr.eval assign).getLsb idx := by
|
||||
(expr.eval assign).getLsbD idx := by
|
||||
intro idx hidx
|
||||
induction expr generalizing aig idx with
|
||||
| const =>
|
||||
|
|
@ -67,13 +67,13 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
|
|||
simp [go, hidx, denote_blastVar]
|
||||
| zeroExtend v inner ih =>
|
||||
simp only [go, denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right,
|
||||
eval_zeroExtend, BitVec.getLsb_zeroExtend, hidx, decide_True, Bool.true_and,
|
||||
eval_zeroExtend, BitVec.getLsbD_zeroExtend, hidx, decide_True, Bool.true_and,
|
||||
Bool.and_iff_right_iff_imp, decide_eq_true_eq]
|
||||
apply BitVec.lt_of_getLsb
|
||||
apply BitVec.lt_of_getLsbD
|
||||
| append lhs rhs lih rih =>
|
||||
rename_i lw rw
|
||||
simp only [go, denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append,
|
||||
BitVec.getLsb_append]
|
||||
BitVec.getLsbD_append]
|
||||
split
|
||||
· next hsplit =>
|
||||
simp only [hsplit, decide_True, cond_true]
|
||||
|
|
@ -95,9 +95,9 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
|
|||
simp only [eval_signExtend]
|
||||
rw [BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false]
|
||||
· simp only [denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right,
|
||||
BitVec.getLsb_zeroExtend, hidx, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp,
|
||||
BitVec.getLsbD_zeroExtend, hidx, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp,
|
||||
decide_eq_true_eq]
|
||||
apply BitVec.lt_of_getLsb
|
||||
apply BitVec.lt_of_getLsbD
|
||||
· subst heq
|
||||
rw [BitVec.msb_zero_length]
|
||||
· simp [heq]
|
||||
|
|
@ -105,23 +105,23 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
|
|||
rw [← hgo]
|
||||
rw [denote_blastSignExtend]
|
||||
simp only [eval_signExtend]
|
||||
rw [BitVec.getLsb_signExtend]
|
||||
rw [BitVec.getLsbD_signExtend]
|
||||
· simp only [hidx, decide_True, Bool.true_and]
|
||||
split
|
||||
· rw [ih]
|
||||
· rw [BitVec.msb_eq_getLsb_last]
|
||||
· rw [BitVec.msb_eq_getLsbD_last]
|
||||
rw [ih]
|
||||
· dsimp only; omega
|
||||
| extract hi lo inner ih =>
|
||||
simp only [go, denote_blastExtract, Bool.if_false_right, eval_extract,
|
||||
BitVec.getLsb_extract]
|
||||
BitVec.getLsbD_extract]
|
||||
have : idx ≤ hi - lo := by omega
|
||||
simp only [this, decide_True, Bool.true_and]
|
||||
split
|
||||
· next hsplit =>
|
||||
rw [ih]
|
||||
· apply Eq.symm
|
||||
apply BitVec.getLsb_ge
|
||||
apply BitVec.getLsbD_ge
|
||||
omega
|
||||
| shiftLeft lhs rhs lih rih =>
|
||||
simp only [go, eval_shiftLeft]
|
||||
|
|
@ -151,21 +151,21 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
|
|||
cases op with
|
||||
| and =>
|
||||
simp only [go, RefVec.denote_zip, denote_mkAndCached, rih, eval_bin, BVBinOp.eval_and,
|
||||
BitVec.getLsb_and]
|
||||
BitVec.getLsbD_and]
|
||||
simp only [go_val_eq_bitblast, RefVec.get_cast]
|
||||
rw [AIG.LawfulVecOperator.denote_input_vec (f := bitblast)]
|
||||
rw [← go_val_eq_bitblast]
|
||||
rw [lih]
|
||||
| or =>
|
||||
simp only [go, RefVec.denote_zip, denote_mkOrCached, rih, eval_bin, BVBinOp.eval_or,
|
||||
BitVec.getLsb_or]
|
||||
BitVec.getLsbD_or]
|
||||
simp only [go_val_eq_bitblast, RefVec.get_cast]
|
||||
rw [AIG.LawfulVecOperator.denote_input_vec (f := bitblast)]
|
||||
rw [← go_val_eq_bitblast]
|
||||
rw [lih]
|
||||
| xor =>
|
||||
simp only [go, RefVec.denote_zip, denote_mkXorCached, rih, eval_bin, BVBinOp.eval_xor,
|
||||
BitVec.getLsb_xor]
|
||||
BitVec.getLsbD_xor]
|
||||
simp only [go_val_eq_bitblast, RefVec.get_cast]
|
||||
rw [AIG.LawfulVecOperator.denote_input_vec (f := bitblast)]
|
||||
rw [← go_val_eq_bitblast]
|
||||
|
|
@ -200,17 +200,17 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
|
|||
| shiftLeftConst => simp [go, ih, hidx]
|
||||
| shiftRightConst =>
|
||||
simp only [go, denote_blastShiftRightConst, ih, dite_eq_ite, Bool.if_false_right, eval_un,
|
||||
BVUnOp.eval_shiftRightConst, BitVec.getLsb_ushiftRight, Bool.and_iff_right_iff_imp,
|
||||
BVUnOp.eval_shiftRightConst, BitVec.getLsbD_ushiftRight, Bool.and_iff_right_iff_imp,
|
||||
decide_eq_true_eq]
|
||||
intro h
|
||||
apply BitVec.lt_of_getLsb
|
||||
apply BitVec.lt_of_getLsbD
|
||||
assumption
|
||||
| rotateLeft => simp [go, ih, hidx]
|
||||
| rotateRight => simp [go, ih, hidx]
|
||||
| arithShiftRightConst n =>
|
||||
rename_i w
|
||||
have : ¬(w ≤ idx) := by omega
|
||||
simp [go, ih, this, BitVec.getLsb_sshiftRight, BitVec.msb_eq_getLsb_last ]
|
||||
simp [go, ih, this, BitVec.getLsbD_sshiftRight, BitVec.msb_eq_getLsbD_last ]
|
||||
|
||||
end bitblast
|
||||
|
||||
|
|
@ -219,7 +219,7 @@ theorem denote_bitblast (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment
|
|||
∀ (idx : Nat) (hidx : idx < w),
|
||||
⟦(bitblast aig expr).aig, (bitblast aig expr).vec.get idx hidx, assign.toAIGAssignment⟧
|
||||
=
|
||||
(expr.eval assign).getLsb idx
|
||||
(expr.eval assign).getLsbD idx
|
||||
:= by
|
||||
intros
|
||||
rw [← bitblast.go_val_eq_bitblast]
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
|
|||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Append
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Eq
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Extract
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.GetLsb
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.GetLsbD
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Not
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Replicate
|
||||
|
|
|
|||
|
|
@ -144,8 +144,8 @@ theorem atLeastTwo_eq_halfAdder (lhsBit rhsBit carry : Bool) :
|
|||
theorem go_denote_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig)
|
||||
(s : AIG.RefVec aig curr) (lhs rhs : AIG.RefVec aig w) (assign : α → Bool)
|
||||
(lhsExpr rhsExpr : BitVec w)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign⟧ = lhsExpr.getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign⟧ = rhsExpr.getLsb idx)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign⟧ = lhsExpr.getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign⟧ = rhsExpr.getLsbD idx)
|
||||
(hcin : ⟦aig, cin, assign⟧ = BitVec.carry curr lhsExpr rhsExpr false) :
|
||||
∀ (idx : Nat) (hidx1 : idx < w),
|
||||
curr ≤ idx
|
||||
|
|
@ -211,14 +211,14 @@ end blastAdd
|
|||
|
||||
theorem denote_blastAdd (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
|
||||
(input : BinaryRefVec aig w)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsb idx) :
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
|
||||
∀ (idx : Nat) (hidx : idx < w),
|
||||
⟦(blastAdd aig input).aig, (blastAdd aig input).vec.get idx hidx, assign⟧
|
||||
=
|
||||
(lhs + rhs).getLsb idx := by
|
||||
(lhs + rhs).getLsbD idx := by
|
||||
intro idx hidx
|
||||
rw [BitVec.getLsb_add]
|
||||
rw [BitVec.getLsbD_add]
|
||||
· rw [← hleft idx hidx]
|
||||
rw [← hright idx hidx]
|
||||
unfold blastAdd
|
||||
|
|
|
|||
|
|
@ -22,8 +22,8 @@ variable [Hashable α] [DecidableEq α]
|
|||
|
||||
theorem mkEq_denote_eq (aig : AIG α) (pair : AIG.BinaryRefVec aig w) (assign : α → Bool)
|
||||
(lhs rhs : BitVec w)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, pair.lhs.get idx hidx, assign⟧ = lhs.getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, pair.rhs.get idx hidx, assign⟧ = rhs.getLsb idx) :
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, pair.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, pair.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
|
||||
⟦mkEq aig pair, assign⟧ = (lhs == rhs) := by
|
||||
unfold mkEq
|
||||
rw [Bool.eq_iff_iff]
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ Authors: Henrik Böving
|
|||
-/
|
||||
prelude
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Basic
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsb
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
|
||||
|
||||
/-!
|
||||
This module contains the verification of the `BitVec.getLsb` bitblaster from `Impl.Operations.Extract`.
|
||||
|
|
@ -21,16 +21,16 @@ namespace BVPred
|
|||
variable [Hashable α] [DecidableEq α]
|
||||
|
||||
@[simp]
|
||||
theorem denote_blastGetLsb (aig : AIG α) (target : GetLsbTarget aig)
|
||||
theorem denote_blastGetLsbD (aig : AIG α) (target : GetLsbDTarget aig)
|
||||
(assign : α → Bool) :
|
||||
⟦blastGetLsb aig target, assign⟧
|
||||
⟦blastGetLsbD aig target, assign⟧
|
||||
=
|
||||
if h : target.idx < target.w then
|
||||
⟦aig, target.vec.get target.idx h, assign⟧
|
||||
else
|
||||
false := by
|
||||
rcases target with ⟨expr, idx⟩
|
||||
unfold blastGetLsb
|
||||
unfold blastGetLsbD
|
||||
dsimp only
|
||||
split <;> simp
|
||||
|
||||
|
|
@ -27,12 +27,12 @@ namespace blastMul
|
|||
|
||||
theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1 ≤ w)
|
||||
(acc : AIG.RefVec aig w) (lhs rhs : AIG.RefVec aig w) (lexpr rexpr : BitVec w) (assign : Assignment)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign.toAIGAssignment⟧ = lexpr.getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign.toAIGAssignment⟧ = rexpr.getLsb idx)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, lhs.get idx hidx, assign.toAIGAssignment⟧ = lexpr.getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, rhs.get idx hidx, assign.toAIGAssignment⟧ = rexpr.getLsbD idx)
|
||||
(hacc : ∀ (idx : Nat) (hidx : idx < w),
|
||||
⟦aig, acc.get idx hidx, assign.toAIGAssignment⟧
|
||||
=
|
||||
(BitVec.mulRec lexpr rexpr curr).getLsb idx) :
|
||||
(BitVec.mulRec lexpr rexpr curr).getLsbD idx) :
|
||||
∀ (idx : Nat) (hidx : idx < w),
|
||||
⟦
|
||||
(go aig lhs rhs (curr + 1) hcurr acc).aig,
|
||||
|
|
@ -40,7 +40,7 @@ theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1
|
|||
assign.toAIGAssignment
|
||||
⟧
|
||||
=
|
||||
(BitVec.mulRec lexpr rexpr w).getLsb idx := by
|
||||
(BitVec.mulRec lexpr rexpr w).getLsbD idx := by
|
||||
intro idx hidx
|
||||
generalize hgo: go aig lhs rhs (curr + 1) hcurr acc = res
|
||||
unfold go at hgo
|
||||
|
|
@ -65,7 +65,7 @@ theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1
|
|||
simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, BitVec.ofNat_eq_ofNat]
|
||||
split
|
||||
· next hdiscr =>
|
||||
have : rexpr.getLsb (curr + 1) = true := by
|
||||
have : rexpr.getLsbD (curr + 1) = true := by
|
||||
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)] at hdiscr
|
||||
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] at hdiscr
|
||||
rw [hright] at hdiscr
|
||||
|
|
@ -77,14 +77,14 @@ theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1
|
|||
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)]
|
||||
rw [hacc]
|
||||
· intros
|
||||
simp only [denote_blastShiftLeftConst, BitVec.getLsb_shiftLeft]
|
||||
simp only [denote_blastShiftLeftConst, BitVec.getLsbD_shiftLeft]
|
||||
split
|
||||
· next hdiscr => simp [hdiscr]
|
||||
· next hidx hdiscr =>
|
||||
rw [hleft]
|
||||
simp [hdiscr, hidx]
|
||||
· next hdiscr =>
|
||||
have : rexpr.getLsb (curr + 1) = false := by
|
||||
have : rexpr.getLsbD (curr + 1) = false := by
|
||||
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)] at hdiscr
|
||||
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] at hdiscr
|
||||
rw [hright] at hdiscr
|
||||
|
|
@ -98,8 +98,8 @@ theorem go_denote_eq {w : Nat} (aig : AIG BVBit) (curr : Nat) (hcurr : curr + 1
|
|||
rw [← hgo]
|
||||
rw [hacc]
|
||||
rw [BitVec.mulRec_succ_eq]
|
||||
have : rexpr.getLsb (curr + 1) = false := by
|
||||
apply BitVec.getLsb_ge
|
||||
have : rexpr.getLsbD (curr + 1) = false := by
|
||||
apply BitVec.getLsbD_ge
|
||||
omega
|
||||
simp [this]
|
||||
termination_by w - curr
|
||||
|
|
@ -112,14 +112,14 @@ end blastMul
|
|||
|
||||
theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment)
|
||||
(input : BinaryRefVec aig w)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign.toAIGAssignment⟧ = lhs.getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign.toAIGAssignment⟧ = rhs.getLsb idx) :
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign.toAIGAssignment⟧ = lhs.getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign.toAIGAssignment⟧ = rhs.getLsbD idx) :
|
||||
∀ (idx : Nat) (hidx : idx < w),
|
||||
⟦(blastMul aig input).aig, (blastMul aig input).vec.get idx hidx, assign.toAIGAssignment⟧
|
||||
=
|
||||
(lhs * rhs).getLsb idx := by
|
||||
(lhs * rhs).getLsbD idx := by
|
||||
intro idx hidx
|
||||
rw [BitVec.getLsb_mul]
|
||||
rw [BitVec.getLsbD_mul]
|
||||
generalize hb : blastMul aig input = res
|
||||
unfold blastMul at hb
|
||||
dsimp only at hb
|
||||
|
|
@ -145,7 +145,7 @@ theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignm
|
|||
rw [BitVec.mulRec_zero_eq]
|
||||
simp only [Nat.succ_eq_add_one, RefVec.denote_ite, BinaryRefVec.rhs_get_cast,
|
||||
Ref.gate_cast, BinaryRefVec.lhs_get_cast, denote_blastConst,
|
||||
BitVec.ofNat_eq_ofNat, eval_const, BitVec.getLsb_zero, Bool.if_false_right,
|
||||
BitVec.ofNat_eq_ofNat, eval_const, BitVec.getLsbD_zero, Bool.if_false_right,
|
||||
Bool.decide_eq_true]
|
||||
split
|
||||
· next heq =>
|
||||
|
|
|
|||
|
|
@ -173,8 +173,8 @@ namespace blastShiftLeft
|
|||
|
||||
theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : BitVec w)
|
||||
(rhs : BitVec target.n) (assign : α → Bool)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, target.lhs.get idx hidx, assign⟧ = lhs.getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.rhs.get idx hidx, assign⟧ = rhs.getLsb idx) :
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, target.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
|
||||
∀ (idx : Nat) (hidx : idx < w),
|
||||
⟦
|
||||
(twoPowShift aig target).aig,
|
||||
|
|
@ -182,7 +182,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
|
|||
assign
|
||||
⟧
|
||||
=
|
||||
(lhs <<< (rhs &&& BitVec.twoPow target.n target.pow)).getLsb idx := by
|
||||
(lhs <<< (rhs &&& BitVec.twoPow target.n target.pow)).getLsbD idx := by
|
||||
intro idx hidx
|
||||
generalize hg : twoPowShift aig target = res
|
||||
rcases target with ⟨n, lvec, rvec, pow⟩
|
||||
|
|
@ -202,14 +202,14 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
|
|||
apply Nat.mod_eq_of_lt
|
||||
apply Nat.pow_lt_pow_of_lt <;> omega
|
||||
split
|
||||
· simp only [BitVec.shiftLeft_eq', BitVec.toNat_twoPow, BitVec.getLsb_shiftLeft,
|
||||
· simp only [BitVec.shiftLeft_eq', BitVec.toNat_twoPow, BitVec.getLsbD_shiftLeft,
|
||||
Bool.false_eq, Bool.and_eq_false_imp, Bool.and_eq_true, decide_eq_true_eq,
|
||||
Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, and_imp]
|
||||
intros
|
||||
apply BitVec.getLsb_ge
|
||||
apply BitVec.getLsbD_ge
|
||||
omega
|
||||
· rw [hleft]
|
||||
simp only [BitVec.shiftLeft_eq', BitVec.toNat_twoPow, hmod, BitVec.getLsb_shiftLeft, hidx,
|
||||
simp only [BitVec.shiftLeft_eq', BitVec.toNat_twoPow, hmod, BitVec.getLsbD_shiftLeft, hidx,
|
||||
decide_True, Bool.true_and, Bool.iff_and_self, Bool.not_eq_true', decide_eq_false_iff_not,
|
||||
Nat.not_lt]
|
||||
omega
|
||||
|
|
@ -224,8 +224,8 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
|
|||
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)]
|
||||
rw [hleft]
|
||||
simp
|
||||
· have : rhs.getLsb pow = false := by
|
||||
apply BitVec.getLsb_ge
|
||||
· have : rhs.getLsbD pow = false := by
|
||||
apply BitVec.getLsbD_ge
|
||||
dsimp only
|
||||
omega
|
||||
simp only [this, Bool.false_eq_true, ↓reduceIte]
|
||||
|
|
@ -236,8 +236,8 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
|
|||
theorem go_denote_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
|
||||
(hcurr : curr ≤ n - 1) (acc : AIG.RefVec aig w)
|
||||
(lhs : BitVec w) (rhs : BitVec n) (assign : α → Bool)
|
||||
(hacc : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, acc.get idx hidx, assign⟧ = (BitVec.shiftLeftRec lhs rhs curr).getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < n), ⟦aig, distance.get idx hidx, assign⟧ = rhs.getLsb idx) :
|
||||
(hacc : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, acc.get idx hidx, assign⟧ = (BitVec.shiftLeftRec lhs rhs curr).getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < n), ⟦aig, distance.get idx hidx, assign⟧ = rhs.getLsbD idx) :
|
||||
∀ (idx : Nat) (hidx : idx < w),
|
||||
⟦
|
||||
(go aig distance curr hcurr acc).aig,
|
||||
|
|
@ -245,7 +245,7 @@ theorem go_denote_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
|
|||
assign
|
||||
⟧
|
||||
=
|
||||
(BitVec.shiftLeftRec lhs rhs (n - 1)).getLsb idx := by
|
||||
(BitVec.shiftLeftRec lhs rhs (n - 1)).getLsbD idx := by
|
||||
intro idx hidx
|
||||
generalize hgo : go aig distance curr hcurr acc = res
|
||||
unfold go at hgo
|
||||
|
|
@ -271,8 +271,8 @@ end blastShiftLeft
|
|||
|
||||
theorem denote_blastShiftLeft (aig : AIG α) (target : ArbitraryShiftTarget aig w0)
|
||||
(lhs : BitVec w0) (rhs : BitVec target.n) (assign : α → Bool)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦aig, target.target.get idx hidx, assign⟧ = lhs.getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.distance.get idx hidx, assign⟧ = rhs.getLsb idx) :
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦aig, target.target.get idx hidx, assign⟧ = lhs.getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.distance.get idx hidx, assign⟧ = rhs.getLsbD idx) :
|
||||
∀ (idx : Nat) (hidx : idx < w0),
|
||||
⟦
|
||||
(blastShiftLeft aig target).aig,
|
||||
|
|
@ -280,7 +280,7 @@ theorem denote_blastShiftLeft (aig : AIG α) (target : ArbitraryShiftTarget aig
|
|||
assign
|
||||
⟧
|
||||
=
|
||||
(lhs <<< rhs).getLsb idx := by
|
||||
(lhs <<< rhs).getLsbD idx := by
|
||||
intro idx hidx
|
||||
rw [BitVec.shiftLeft_eq_shiftLeftRec]
|
||||
generalize hg : blastShiftLeft aig target = res
|
||||
|
|
@ -293,10 +293,10 @@ theorem denote_blastShiftLeft (aig : AIG α) (target : ArbitraryShiftTarget aig
|
|||
subst hzero
|
||||
rw [← hg]
|
||||
simp only [hleft, Nat.zero_sub, BitVec.shiftLeftRec_zero, BitVec.and_twoPow, Nat.le_refl,
|
||||
BitVec.getLsb_ge, Bool.false_eq_true, ↓reduceIte, BitVec.reduceHShiftLeft',
|
||||
BitVec.getLsb_shiftLeft, Nat.sub_zero, Bool.iff_and_self, Bool.and_eq_true, decide_eq_true_eq,
|
||||
BitVec.getLsbD_ge, Bool.false_eq_true, ↓reduceIte, BitVec.reduceHShiftLeft',
|
||||
BitVec.getLsbD_shiftLeft, Nat.sub_zero, Bool.iff_and_self, Bool.and_eq_true, decide_eq_true_eq,
|
||||
Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, Nat.zero_le, and_true]
|
||||
apply BitVec.lt_of_getLsb
|
||||
apply BitVec.lt_of_getLsbD
|
||||
· rw [← hg]
|
||||
rw [blastShiftLeft.go_denote_eq]
|
||||
· intro idx hidx
|
||||
|
|
|
|||
|
|
@ -262,8 +262,8 @@ namespace blastShiftRight
|
|||
|
||||
theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : BitVec w)
|
||||
(rhs : BitVec target.n) (assign : α → Bool)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, target.lhs.get idx hidx, assign⟧ = lhs.getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.rhs.get idx hidx, assign⟧ = rhs.getLsb idx) :
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, target.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
|
||||
∀ (idx : Nat) (hidx : idx < w),
|
||||
⟦
|
||||
(twoPowShift aig target).aig,
|
||||
|
|
@ -271,7 +271,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
|
|||
assign
|
||||
⟧
|
||||
=
|
||||
(lhs >>> (rhs &&& BitVec.twoPow target.n target.pow)).getLsb idx := by
|
||||
(lhs >>> (rhs &&& BitVec.twoPow target.n target.pow)).getLsbD idx := by
|
||||
intro idx hidx
|
||||
generalize hg : twoPowShift aig target = res
|
||||
rcases target with ⟨n, lvec, rvec, pow⟩
|
||||
|
|
@ -293,9 +293,9 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
|
|||
split
|
||||
· rw [hleft]
|
||||
simp [hmod]
|
||||
· simp only [BitVec.ushiftRight_eq', BitVec.toNat_twoPow, BitVec.getLsb_ushiftRight,
|
||||
· simp only [BitVec.ushiftRight_eq', BitVec.toNat_twoPow, BitVec.getLsbD_ushiftRight,
|
||||
Bool.false_eq]
|
||||
apply BitVec.getLsb_ge
|
||||
apply BitVec.getLsbD_ge
|
||||
omega
|
||||
· next hif1 =>
|
||||
simp only [Bool.not_eq_true] at hif1
|
||||
|
|
@ -308,8 +308,8 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
|
|||
rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst)]
|
||||
rw [hleft]
|
||||
simp
|
||||
· have : rhs.getLsb pow = false := by
|
||||
apply BitVec.getLsb_ge
|
||||
· have : rhs.getLsbD pow = false := by
|
||||
apply BitVec.getLsbD_ge
|
||||
dsimp only
|
||||
omega
|
||||
simp only [this, Bool.false_eq_true, ↓reduceIte]
|
||||
|
|
@ -320,8 +320,8 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
|
|||
theorem go_denote_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
|
||||
(hcurr : curr ≤ n - 1) (acc : AIG.RefVec aig w)
|
||||
(lhs : BitVec w) (rhs : BitVec n) (assign : α → Bool)
|
||||
(hacc : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, acc.get idx hidx, assign⟧ = (BitVec.ushiftRightRec lhs rhs curr).getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < n), ⟦aig, distance.get idx hidx, assign⟧ = rhs.getLsb idx) :
|
||||
(hacc : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, acc.get idx hidx, assign⟧ = (BitVec.ushiftRightRec lhs rhs curr).getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < n), ⟦aig, distance.get idx hidx, assign⟧ = rhs.getLsbD idx) :
|
||||
∀ (idx : Nat) (hidx : idx < w),
|
||||
⟦
|
||||
(go aig distance curr hcurr acc).aig,
|
||||
|
|
@ -329,7 +329,7 @@ theorem go_denote_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
|
|||
assign
|
||||
⟧
|
||||
=
|
||||
(BitVec.ushiftRightRec lhs rhs (n - 1)).getLsb idx := by
|
||||
(BitVec.ushiftRightRec lhs rhs (n - 1)).getLsbD idx := by
|
||||
intro idx hidx
|
||||
generalize hgo : go aig distance curr hcurr acc = res
|
||||
unfold go at hgo
|
||||
|
|
@ -355,8 +355,8 @@ end blastShiftRight
|
|||
|
||||
theorem denote_blastShiftRight (aig : AIG α) (target : ArbitraryShiftTarget aig w0)
|
||||
(lhs : BitVec w0) (rhs : BitVec target.n) (assign : α → Bool)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦aig, target.target.get idx hidx, assign⟧ = lhs.getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.distance.get idx hidx, assign⟧ = rhs.getLsb idx) :
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦aig, target.target.get idx hidx, assign⟧ = lhs.getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.distance.get idx hidx, assign⟧ = rhs.getLsbD idx) :
|
||||
∀ (idx : Nat) (hidx : idx < w0),
|
||||
⟦
|
||||
(blastShiftRight aig target).aig,
|
||||
|
|
@ -364,7 +364,7 @@ theorem denote_blastShiftRight (aig : AIG α) (target : ArbitraryShiftTarget aig
|
|||
assign
|
||||
⟧
|
||||
=
|
||||
(lhs >>> rhs).getLsb idx := by
|
||||
(lhs >>> rhs).getLsbD idx := by
|
||||
intro idx hidx
|
||||
rw [BitVec.shiftRight_eq_ushiftRightRec]
|
||||
generalize hres : blastShiftRight aig target = res
|
||||
|
|
|
|||
|
|
@ -24,8 +24,8 @@ variable [Hashable α] [DecidableEq α]
|
|||
|
||||
theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVec aig w)
|
||||
(assign : α → Bool)
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsb idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsb idx) :
|
||||
(hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
|
||||
(hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
|
||||
⟦(mkUlt aig input).aig, (mkUlt aig input).ref, assign⟧ = BitVec.ult lhs rhs := by
|
||||
rw [BitVec.ult_eq_not_carry]
|
||||
unfold mkUlt
|
||||
|
|
@ -42,7 +42,7 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe
|
|||
· dsimp only
|
||||
intro idx hidx
|
||||
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
|
||||
· simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsb_not, hidx, decide_True,
|
||||
· simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsbD_not, hidx, decide_True,
|
||||
Bool.true_and]
|
||||
rw [BVExpr.bitblast.denote_blastNot]
|
||||
congr 1
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ Authors: Henrik Böving
|
|||
prelude
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Eq
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Ult
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.GetLsb
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.GetLsbD
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
|
||||
import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
|
||||
|
||||
|
|
@ -48,10 +48,10 @@ theorem denote_bitblast (aig : AIG BVBit) (pred : BVPred) (assign : BVExpr.Assig
|
|||
· simp [Ref.hgate]
|
||||
· intros
|
||||
simp
|
||||
| getLsb expr idx =>
|
||||
simp only [bitblast, denote_blastGetLsb, BVExpr.denote_bitblast, dite_eq_ite,
|
||||
Bool.if_false_right, eval_getLsb, Bool.and_iff_right_iff_imp, decide_eq_true_eq]
|
||||
apply BitVec.lt_of_getLsb
|
||||
| getLsbD expr idx =>
|
||||
simp only [bitblast, denote_blastGetLsbD, BVExpr.denote_bitblast, dite_eq_ite,
|
||||
Bool.if_false_right, eval_getLsbD, Bool.and_iff_right_iff_imp, decide_eq_true_eq]
|
||||
apply BitVec.lt_of_getLsbD
|
||||
|
||||
end BVPred
|
||||
|
||||
|
|
|
|||
|
|
@ -85,7 +85,7 @@ theorem go_denote_eq (aig : AIG BVBit) (a : Nat) (assign : Assignment) (curr : N
|
|||
assign.toAIGAssignment
|
||||
⟧
|
||||
=
|
||||
((BVExpr.var (w := w) a).eval assign).getLsb idx := by
|
||||
((BVExpr.var (w := w) a).eval assign).getLsbD idx := by
|
||||
intro idx hidx1 hidx2
|
||||
generalize hgo : go aig w a curr s hcurr = res
|
||||
unfold go at hgo
|
||||
|
|
@ -118,7 +118,7 @@ theorem denote_blastVar (aig : AIG BVBit) (var : BVVar w) (assign : Assignment)
|
|||
∀ (idx : Nat) (hidx : idx < w),
|
||||
⟦(blastVar aig var).aig, (blastVar aig var).vec.get idx hidx, assign.toAIGAssignment⟧
|
||||
=
|
||||
((BVExpr.var (w := w) var.ident).eval assign).getLsb idx := by
|
||||
((BVExpr.var (w := w) var.ident).eval assign).getLsbD idx := by
|
||||
intros
|
||||
apply blastVar.go_denote_eq
|
||||
omega
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ attribute [bv_normalize] ge_iff_le
|
|||
theorem BitVec.truncate_eq_zeroExtend (x : BitVec w) : x.truncate n = x.zeroExtend n := by
|
||||
rfl
|
||||
|
||||
attribute [bv_normalize] BitVec.msb_eq_getLsb_last
|
||||
attribute [bv_normalize] BitVec.msb_eq_getLsbD_last
|
||||
attribute [bv_normalize] BitVec.slt_eq_ult
|
||||
attribute [bv_normalize] BitVec.sle_eq_not_slt
|
||||
|
||||
|
|
@ -57,9 +57,9 @@ attribute [bv_normalize] BitVec.sub_self
|
|||
attribute [bv_normalize] BitVec.sub_zero
|
||||
attribute [bv_normalize] BitVec.zeroExtend_eq
|
||||
attribute [bv_normalize] BitVec.zeroExtend_zero
|
||||
attribute [bv_normalize] BitVec.getLsb_zero
|
||||
attribute [bv_normalize] BitVec.getLsb_zero_length
|
||||
attribute [bv_normalize] BitVec.getLsb_concat_zero
|
||||
attribute [bv_normalize] BitVec.getLsbD_zero
|
||||
attribute [bv_normalize] BitVec.getLsbD_zero_length
|
||||
attribute [bv_normalize] BitVec.getLsbD_concat_zero
|
||||
attribute [bv_normalize] BitVec.mul_one
|
||||
attribute [bv_normalize] BitVec.one_mul
|
||||
|
||||
|
|
@ -123,12 +123,12 @@ theorem BitVec.neg_add (a : BitVec w) : (-a) + a = 0#w := by
|
|||
@[bv_normalize]
|
||||
theorem BitVec.zero_sshiftRight : BitVec.sshiftRight 0#w a = 0#w := by
|
||||
ext
|
||||
simp [BitVec.getLsb_sshiftRight]
|
||||
simp [BitVec.getLsbD_sshiftRight]
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.sshiftRight_zero : BitVec.sshiftRight a 0 = a := by
|
||||
ext
|
||||
simp [BitVec.getLsb_sshiftRight]
|
||||
simp [BitVec.getLsbD_sshiftRight]
|
||||
|
||||
@[bv_normalize]
|
||||
theorem BitVec.mul_zero (a : BitVec w) : a * 0#w = 0#w := by
|
||||
|
|
|
|||
|
|
@ -75,7 +75,7 @@ theorem Bool.decide_eq_true (a : Bool) : (decide (a = true)) = a := by
|
|||
theorem Bool.eq_true_eq_true_eq (x y : Bool) : ((x = true) = (y = true)) = (x = y) :=
|
||||
by simp
|
||||
|
||||
attribute [bv_normalize] BitVec.getLsb_cast
|
||||
attribute [bv_normalize] BitVec.getLsbD_cast
|
||||
attribute [bv_normalize] BitVec.testBit_toNat
|
||||
|
||||
@[bv_normalize]
|
||||
|
|
|
|||
|
|
@ -103,11 +103,11 @@ theorem ult_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' =
|
|||
(BitVec.ult lhs' rhs') = (BitVec.ult lhs rhs) := by
|
||||
simp[*]
|
||||
|
||||
theorem getLsb_congr (i : Nat) (w : Nat) (e e' : BitVec w) (h : e' = e) :
|
||||
(e'.getLsb i) = (e.getLsb i) := by
|
||||
theorem getLsbD_congr (i : Nat) (w : Nat) (e e' : BitVec w) (h : e' = e) :
|
||||
(e'.getLsbD i) = (e.getLsbD i) := by
|
||||
simp[*]
|
||||
|
||||
theorem ofBool_congr (b : Bool) (e' : BitVec 1) (h : e' = BitVec.ofBool b) : e'.getLsb 0 = b := by
|
||||
theorem ofBool_congr (b : Bool) (e' : BitVec 1) (h : e' = BitVec.ofBool b) : e'.getLsbD 0 = b := by
|
||||
cases b <;> simp [h]
|
||||
|
||||
end BitVec
|
||||
|
|
|
|||
|
|
@ -30,21 +30,21 @@
|
|||
"position": {"line": 9, "character": 11}},
|
||||
"id": {"const": {"declName": "instToBoolBool"}}}},
|
||||
{"sortText": "2",
|
||||
"label": "BitVec.getLsb_ofBoolListBE",
|
||||
"label": "BitVec.getLsbD_ofBoolListBE",
|
||||
"kind": 3,
|
||||
"data":
|
||||
{"params":
|
||||
{"textDocument": {"uri": "file:///completionPrv.lean"},
|
||||
"position": {"line": 9, "character": 11}},
|
||||
"id": {"const": {"declName": "BitVec.getLsb_ofBoolListBE"}}}},
|
||||
"id": {"const": {"declName": "BitVec.getLsbD_ofBoolListBE"}}}},
|
||||
{"sortText": "3",
|
||||
"label": "BitVec.getMsb_ofBoolListBE",
|
||||
"label": "BitVec.getMsbD_ofBoolListBE",
|
||||
"kind": 3,
|
||||
"data":
|
||||
{"params":
|
||||
{"textDocument": {"uri": "file:///completionPrv.lean"},
|
||||
"position": {"line": 9, "character": 11}},
|
||||
"id": {"const": {"declName": "BitVec.getMsb_ofBoolListBE"}}}},
|
||||
"id": {"const": {"declName": "BitVec.getMsbD_ofBoolListBE"}}}},
|
||||
{"sortText": "4",
|
||||
"label": "BitVec.ofBoolListBE",
|
||||
"kind": 3,
|
||||
|
|
|
|||
|
|
@ -43,13 +43,13 @@ example (h : x = (1 : BitVec 32)) : x = - smtSDiv 9 0 := by
|
|||
simp; guard_target =ₛ x = 1#32; assumption
|
||||
example (h : x = (1 : BitVec 32)) : x = smtSDiv (-9) 0 := by
|
||||
simp; guard_target =ₛ x = 1#32; assumption
|
||||
example (h : x = false) : x = (4#3).getLsb 0:= by
|
||||
example (h : x = false) : x = (4#3).getLsbD 0:= by
|
||||
simp; guard_target =ₛ x = false; assumption
|
||||
example (h : x = true) : x = (4#3).getLsb 2:= by
|
||||
example (h : x = true) : x = (4#3).getLsbD 2:= by
|
||||
simp; guard_target =ₛ x = true; assumption
|
||||
example (h : x = true) : x = (4#3).getMsb 0:= by
|
||||
example (h : x = true) : x = (4#3).getMsbD 0:= by
|
||||
simp; guard_target =ₛ x = true; assumption
|
||||
example (h : x = false) : x = (4#3).getMsb 2:= by
|
||||
example (h : x = false) : x = (4#3).getMsbD 2:= by
|
||||
simp; guard_target =ₛ x = false; assumption
|
||||
example (h : x = (24 : BitVec 32)) : x = 6#32 <<< 2 := by
|
||||
simp; guard_target =ₛ x = 24#32; assumption
|
||||
|
|
|
|||
|
|
@ -14,16 +14,16 @@ theorem bitwise_unit_2 {x : BitVec 64} : x ^^^ x = 0 := by
|
|||
theorem bitwise_unit_2' {x : BitVec 64} : (BitVec.xor x x) = 0 := by
|
||||
bv_decide
|
||||
|
||||
theorem bitwise_unit_3 {x : BitVec 64} : (x ^^^ x).getLsb 32 = false := by
|
||||
theorem bitwise_unit_3 {x : BitVec 64} : (x ^^^ x).getLsbD 32 = false := by
|
||||
bv_decide
|
||||
|
||||
theorem bitwise_unit_4 {x : BitVec 64} : (x ^^^ ~~~x).getLsb 32 = true := by
|
||||
theorem bitwise_unit_4 {x : BitVec 64} : (x ^^^ ~~~x).getLsbD 32 = true := by
|
||||
bv_decide
|
||||
|
||||
theorem bitwise_unit_5 {x : BitVec 64} : (x ^^^ ~~~x).getLsb 128 = false := by
|
||||
theorem bitwise_unit_5 {x : BitVec 64} : (x ^^^ ~~~x).getLsbD 128 = false := by
|
||||
bv_decide
|
||||
|
||||
theorem bitwise_unit_6 {x : BitVec 64} : (x ^^^ ~~~x).getLsb 63 = (x ^^^ ~~~x).msb := by
|
||||
theorem bitwise_unit_6 {x : BitVec 64} : (x ^^^ ~~~x).getLsbD 63 = (x ^^^ ~~~x).msb := by
|
||||
bv_decide
|
||||
|
||||
theorem bitwise_unit_7 (x : BitVec 32) : x ^^^ 123#32 = 123#'(by decide) ^^^ x := by
|
||||
|
|
|
|||
|
|
@ -35,5 +35,5 @@ theorem cast_unit_8 (x : BitVec 64) : (x.signExtend 128 = x.zeroExtend 128) ↔
|
|||
theorem cast_unit_9 (x : BitVec 32) : (x.replicate 20).zeroExtend 32 = x := by
|
||||
bv_decide
|
||||
|
||||
theorem cast_unit_10 (x : BitVec 32) : (x.replicate 20).getLsb 40 = x.getLsb 8 := by
|
||||
theorem cast_unit_10 (x : BitVec 32) : (x.replicate 20).getLsbD 40 = x.getLsbD 8 := by
|
||||
bv_decide
|
||||
|
|
|
|||
|
|
@ -78,7 +78,7 @@ bool will_add_overflow_bitwise_3(int32_t a_, int32_t b_) {
|
|||
-/
|
||||
def will_add_overflow_bitwise_3 (a b : BitVec 32) : Bool :=
|
||||
let c := a + b
|
||||
getLsb (((~~~a &&& ~~~b &&& c) ||| (a &&& b &&& ~~~c)) >>> 31) 0
|
||||
getLsbD (((~~~a &&& ~~~b &&& c) ||| (a &&& b &&& ~~~c)) >>> 31) 0
|
||||
|
||||
example (a b : BitVec 32) : will_add_overflow_bitwise_2 a b = will_add_overflow_bitwise_3 a b := by
|
||||
dsimp [will_add_overflow_bitwise_2, will_add_overflow_bitwise_3]
|
||||
|
|
@ -93,7 +93,7 @@ bool will_add_overflow_optimized_a(int32_t a_, int32_t b_) {
|
|||
-/
|
||||
def will_add_overflow_optimized_a (a b : BitVec 32) : Bool :=
|
||||
let c := a + b
|
||||
getLsb ((~~~(a ^^^ b) &&& (c ^^^ a)) >>> 31) 0
|
||||
getLsbD ((~~~(a ^^^ b) &&& (c ^^^ a)) >>> 31) 0
|
||||
|
||||
example (a b : BitVec 32) :
|
||||
will_add_overflow_bitwise_3 a b = will_add_overflow_optimized_a a b := by
|
||||
|
|
@ -109,7 +109,7 @@ bool will_add_overflow_optimized_b(int32_t a_, int32_t b_) {
|
|||
-/
|
||||
def will_add_overflow_optimized_b (a b : BitVec 32) : Bool :=
|
||||
let c := a + b
|
||||
getLsb (((c ^^^ a) &&& (c ^^^ b)) >>> 31) 0
|
||||
getLsbD (((c ^^^ a) &&& (c ^^^ b)) >>> 31) 0
|
||||
|
||||
example (a b : BitVec 32) :
|
||||
will_add_overflow_optimized_a a b = will_add_overflow_optimized_b a b := by
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue