feat: BitVec simprocs

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean

@@ -11,3 +11,4 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -0,0 +1,292 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
+import Init.Data.BitVec.Basic
+
+namespace Std.BitVec
+open Lean Meta Simp
+
+/-- A bit-vector literal -/
+structure Literal where
+  /-- Size. -/
+  n     : Nat
+  /-- Actual value. -/
+  value : BitVec n
+
+/--
+Try to convert an `OfNat.ofNat`-application into a bitvector literal.
+-/
+private def fromOfNatExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isAppOfArity ``BitVec 1)
+  let n ← Nat.fromExpr? type.appArg!
+  let v ← Nat.fromExpr? e.appFn!.appArg!
+  return { n, value := BitVec.ofNat n v }
+
+/--
+Try to convert an `Std.BitVec.ofNat`-application into a bitvector literal.
+-/
+private def fromBitVecExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
+  guard (e.isAppOfArity ``Std.BitVec.ofNat 2)
+  let n ← Nat.fromExpr? e.appFn!.appArg!
+  let v ← Nat.fromExpr? e.appArg!
+  return { n, value := BitVec.ofNat n v }
+
+/--
+Try to convert `OfNat.ofNat`/`Std.BitVec.OfNat` application into a
+bitvector literal.
+-/
+def fromExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
+  fromBitVecExpr? e <|> fromOfNatExpr? e
+
+/--
+Convert a bitvector literal into an expression.
+-/
+-- Using `Std.BitVec.ofNat` because it is being used in `simp` theorems
+def Literal.toExpr (lit : Literal) : Expr :=
+  mkApp2 (mkConst ``Std.BitVec.ofNat) (mkNatLit lit.n) (mkNatLit lit.value.toNat)
+
+/--
+Helper function for reducing homogenous unary bitvector operators.
+-/
+@[inline] def reduceUnary (declName : Name) (arity : Nat)
+    (op : {n : Nat} → BitVec n → BitVec n) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let v := { v with value := op v.value }
+  return .done { expr := v.toExpr }
+
+/--
+Helper function for reducing homogenous binary bitvector operators.
+-/
+@[inline] def reduceBin (declName : Name) (arity : Nat)
+    (op : {n : Nat} → BitVec n → BitVec n → BitVec n) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← fromExpr? e.appArg! | return .continue
+  if h : v₁.n = v₂.n then
+    trace[Meta.debug] "reduce [{declName}] {v₁.value}, {v₂.value}"
+    let v := { v₁ with value := op v₁.value (h ▸ v₂.value) }
+    return .done { expr := v.toExpr }
+  else
+    return .continue
+
+/--
+Helper function for reducing bitvector functions such as `getLsb` and `getMsb`.
+-/
+@[inline] def reduceGetBit (declName : Name) (op : {n : Nat} → BitVec n → Nat → Bool) (e : Expr)
+    : SimpM Step := do
+  unless e.isAppOfArity declName 3 do return .continue
+  let some v ← fromExpr? e.appFn!.appArg! | return .continue
+  let some i ← Nat.fromExpr? e.appArg! | return .continue
+  let b := op v.value i
+  return .done { expr := toExpr b }
+
+/--
+Helper function for reducing bitvector functions such as `shiftLeft` and `rotateRight`.
+-/
+@[inline] def reduceShift (declName : Name) (arity : Nat)
+    (op : {n : Nat} → BitVec n → Nat → BitVec n) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some v ← fromExpr? e.appFn!.appArg! | return .continue
+  let some i ← Nat.fromExpr? e.appArg! | return .continue
+  let v := { v with value := op v.value i }
+  return .done { expr := v.toExpr }
+
+/--
+Helper function for reducing bitvector predicates.
+-/
+@[inline] def reduceBinPred (declName : Name) (arity : Nat)
+    (op : {n : Nat} → BitVec n → BitVec n → Bool) (e : Expr) (isProp := true) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← fromExpr? e.appArg! | return .continue
+  if h : v₁.n = v₂.n then
+    let b := op v₁.value (h ▸ v₂.value)
+    if isProp then
+      evalPropStep e b
+    else
+      return .done { expr := toExpr b }
+  else
+    return .continue
+
+/-- Simplification procedure for negation of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceNeg ((- _ : BitVec _)) := reduceUnary ``Neg.neg 3 (- ·)
+/-- Simplification procedure for bitwise not of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceNot ((~~~ _ : BitVec _)) :=
+  reduceUnary ``Complement.complement 3 (~~~ ·)
+/-- Simplification procedure for absolute value of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceAbs (BitVec.abs _) := reduceUnary ``BitVec.abs 2 BitVec.abs
+/-- Simplification procedure for bitwise and of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceAnd ((_ &&& _ : BitVec _)) := reduceBin ``HAnd.hAnd 6 (· &&& ·)
+/-- Simplification procedure for bitwise or of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceOr ((_ ||| _ : BitVec _)) := reduceBin ``HOr.hOr 6 (· ||| ·)
+/-- Simplification procedure for bitwise xor of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceXOr ((_ ^^^ _ : BitVec _)) := reduceBin ``HXor.hXor 6 (· ^^^ ·)
+/-- Simplification procedure for addition of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceAdd ((_ + _ : BitVec _)) := reduceBin ``HAdd.hAdd 6 (· + ·)
+/-- Simplification procedure for multiplication of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceMul ((_ * _ : BitVec _)) := reduceBin ``HMul.hMul 6 (· * ·)
+/-- Simplification procedure for subtraction of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceSub ((_ - _ : BitVec _)) := reduceBin ``HSub.hSub 6 (· - ·)
+/-- Simplification procedure for division of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceDiv ((_ / _ : BitVec _)) := reduceBin ``HDiv.hDiv 6 (· / ·)
+/-- Simplification procedure for the modulo operation on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceMod ((_ % _ : BitVec _)) := reduceBin ``HMod.hMod 6 (· % ·)
+/-- Simplification procedure for for the unsigned modulo operation on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceUMod ((umod _ _ : BitVec _)) := reduceBin ``umod 3 umod
+/-- Simplification procedure for unsigned division of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceUDiv ((udiv _ _ : BitVec _)) := reduceBin ``udiv 3 udiv
+/-- Simplification procedure for division of `BitVec`s using the SMT-Lib conventions. -/
+builtin_simproc [simp, seval] reduceSMTUDiv ((smtUDiv _ _ : BitVec _)) := reduceBin ``smtUDiv 3 smtUDiv
+/-- Simplification procedure for the signed modulo operation on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceSMod ((smod _ _ : BitVec _)) := reduceBin ``smod 3 smod
+/-- Simplification procedure for signed remainder of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceSRem ((srem _ _ : BitVec _)) := reduceBin ``srem 3 srem
+/-- Simplification procedure for signed t-division of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceSDiv ((sdiv _ _ : BitVec _)) := reduceBin ``sdiv 3 sdiv
+/-- Simplification procedure for signed division of `BitVec`s using the SMT-Lib conventions. -/
+builtin_simproc [simp, seval] reduceSMTSDiv ((smtSDiv _ _ : BitVec _)) := reduceBin ``smtSDiv 3 smtSDiv
+/-- Simplification procedure for `getLsb` (lowest significant bit) on `BitVec`. -/
+builtin_simproc [simp, seval] reduceGetLsb (getLsb _ _) := reduceGetBit ``getLsb getLsb
+/-- Simplification procedure for `getMsb` (most significant bit) on `BitVec`. -/
+builtin_simproc [simp, seval] reduceGetMsb (getMsb _ _) := reduceGetBit ``getMsb getMsb
+
+/-- Simplification procedure for shift left on `BitVec`. -/
+builtin_simproc [simp, seval] reduceShiftLeft (BitVec.shiftLeft _ _) :=
+  reduceShift ``BitVec.shiftLeft 3 BitVec.shiftLeft
+/-- Simplification procedure for unsigned shift right on `BitVec`. -/
+builtin_simproc [simp, seval] reduceUShiftRight (BitVec.ushiftRight _ _) :=
+  reduceShift ``BitVec.ushiftRight 3 BitVec.ushiftRight
+/-- Simplification procedure for signed shift right on `BitVec`. -/
+builtin_simproc [simp, seval] reduceSShiftRight (BitVec.sshiftRight _ _) :=
+  reduceShift ``BitVec.sshiftRight 3 BitVec.sshiftRight
+/-- Simplification procedure for shift left on `BitVec`. -/
+builtin_simproc [simp, seval] reduceHShiftLeft ((_ <<< _ : BitVec _)) :=
+  reduceShift ``HShiftLeft.hShiftLeft 6 (· <<< ·)
+/-- Simplification procedure for shift right on `BitVec`. -/
+builtin_simproc [simp, seval] reduceHShiftRight ((_ >>> _ : BitVec _)) :=
+  reduceShift ``HShiftRight.hShiftRight 6 (· >>> ·)
+/-- Simplification procedure for rotate left on `BitVec`. -/
+builtin_simproc [simp, seval] reduceRotateLeft (BitVec.rotateLeft _ _) :=
+  reduceShift ``BitVec.rotateLeft 3 BitVec.rotateLeft
+/-- Simplification procedure for rotate right on `BitVec`. -/
+builtin_simproc [simp, seval] reduceRotateRight (BitVec.rotateRight _ _) :=
+  reduceShift ``BitVec.rotateRight 3 BitVec.rotateRight
+
+/-- Simplification procedure for append on `BitVec`. -/
+builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : BitVec _)) := fun e => do
+  unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← fromExpr? e.appArg! | return .continue
+  let v : Literal := { n := v₁.n + v₂.n, value := v₁.value ++ v₂.value }
+  return .done { expr := v.toExpr }
+
+/-- Simplification procedure for casting `BitVec`s along an equality of the size. -/
+builtin_simproc [simp, seval] reduceCast (cast _ _) := fun e => do
+  unless e.isAppOfArity ``cast 4 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some m ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
+  let v : Literal := { n := m, value := BitVec.ofNat m v.value.toNat }
+  return .done { expr := v.toExpr }
+
+/-- Simplification procedure for `BitVec.toNat`. -/
+builtin_simproc [simp, seval] reduceToNat (BitVec.toNat _) := fun e => do
+  unless e.isAppOfArity ``BitVec.toNat 2 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  return .done { expr := mkNatLit v.value.toNat }
+
+/-- Simplification procedure for `BitVec.toInt`. -/
+builtin_simproc [simp, seval] reduceToInt (BitVec.toInt _) := fun e => do
+  unless e.isAppOfArity ``BitVec.toInt 2 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  return .done { expr := Int.toExpr v.value.toInt }
+
+/-- Simplification procedure for `BitVec.ofInt`. -/
+builtin_simproc [simp, seval] reduceOfInt (BitVec.ofInt _ _) := fun e => do
+  unless e.isAppOfArity ``BitVec.ofInt 2 do return .continue
+  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let some i ← Int.fromExpr? e.appArg! | return .continue
+  let lit : Literal := { n, value := BitVec.ofInt n i }
+  return .done { expr := lit.toExpr }
+
+/-- Simplification procedure for `<` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceLT (( _ : BitVec _) < _)  := reduceBinPred ``LT.lt 4 (· < ·)
+/-- Simplification procedure for `≤` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceLE (( _ : BitVec _) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+/-- Simplification procedure for `>` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceGT (( _ : BitVec _) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+/-- Simplification procedure for `≥` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceGE (( _ : BitVec _) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+
+/-- Simplification procedure for unsigned less than `ult` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceULT (BitVec.ult _ _) :=
+  reduceBinPred ``BitVec.ult 3 BitVec.ult (isProp := false)
+/-- Simplification procedure for unsigned less than or equal `ule` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceULE (BitVec.ule _ _) :=
+  reduceBinPred ``BitVec.ule 3 BitVec.ule (isProp := false)
+/-- Simplification procedure for signed less than `slt` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceSLT (BitVec.slt _ _) :=
+  reduceBinPred ``BitVec.slt 3 BitVec.slt (isProp := false)
+/-- Simplification procedure for signed less than or equal `sle` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceSLE (BitVec.sle _ _) :=
+  reduceBinPred ``BitVec.sle 3 BitVec.sle (isProp := false)
+
+/-- Simplification procedure for `zeroExtend'` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
+  unless e.isAppOfArity ``zeroExtend' 4 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some w ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
+  if h : v.n ≤ w then
+    let lit : Literal := { n := w, value := v.value.zeroExtend' h }
+    return .done { expr := lit.toExpr }
+  else
+    return .continue
+
+/-- Simplification procedure for `shiftLeftZeroExtend` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceShiftLeftZeroExtend (shiftLeftZeroExtend _ _) := fun e => do
+  unless e.isAppOfArity ``shiftLeftZeroExtend 3 do return .continue
+  let some v ← fromExpr? e.appFn!.appArg! | return .continue
+  let some m ← Nat.fromExpr? e.appArg! | return .continue
+  let lit : Literal := { n := v.n + m, value := v.value.shiftLeftZeroExtend m }
+  return .done { expr := lit.toExpr }
+
+/-- Simplification procedure for `extractLsb'` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => do
+  unless e.isAppOfArity ``extractLsb' 4 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some start ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
+  let some len ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let lit : Literal := { n := len, value := v.value.extractLsb' start len }
+  return .done { expr := lit.toExpr }
+
+/-- Simplification procedure for `replicate` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
+  unless e.isAppOfArity ``replicate 3 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some w ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let lit : Literal := { n := v.n * w, value := v.value.replicate w }
+  return .done { expr := lit.toExpr }
+
+/-- Simplification procedure for `zeroExtend` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := fun e => do
+  unless e.isAppOfArity ``zeroExtend 3 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let lit : Literal := { n, value := v.value.zeroExtend n }
+  return .done { expr := lit.toExpr }
+
+/-- Simplification procedure for `allOnes` -/
+builtin_simproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do
+  unless e.isAppOfArity ``allOnes 1 do return .continue
+  let some n ← Nat.fromExpr? e.appArg! | return .continue
+  let lit : Literal := { n, value := allOnes n }
+  return .done { expr := lit.toExpr }
+
+end Std.BitVec

tests/lean/run/bitvec_simproc.lean

@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+open Std BitVec
+
+example (h : x = (6 : Std.BitVec 3)) : x = -2 := by
+  simp; guard_target =ₛ x = 6#3; assumption
+example (h : x = (5 : Std.BitVec 3)) : x = ~~~2 := by
+  simp; guard_target =ₛ x = 5#3; assumption
+example (h : x = (1 : Std.BitVec 32)) : x = BitVec.abs (-1#32) := by
+  simp; guard_target =ₛ x = 1#32; assumption
+example (h : x = (5 : Std.BitVec 3)) : x = 2 + 3 := by
+  simp; guard_target =ₛ x = 5#3; assumption
+example (h : x = (1 : Std.BitVec 3)) : x = 5 &&& 3 := by
+  simp; guard_target =ₛ x = 1#3; assumption
+example (h : x = (7 : Std.BitVec 3)) : x = 5 ||| 3 := by
+  simp; guard_target =ₛ x = 7#3; assumption
+example (h : x = (6 : Std.BitVec 3)) : x = 5 ^^^ 3 := by
+  simp; guard_target =ₛ x = 6#3; assumption
+example (h : x = (3 : Std.BitVec 32)) : x = 5 - 2 := by
+  simp; guard_target =ₛ x = 3#32; assumption
+example (h : x = (10 : Std.BitVec 32)) : x = 5 * 2 := by
+  simp; guard_target =ₛ x = 10#32; assumption
+example (h : x = (4 : Std.BitVec 32)) : x = 9 / 2 := by
+  simp; guard_target =ₛ x = 4#32; assumption
+example (h : x = (1 : Std.BitVec 32)) : x = 9 % 2 := by
+  simp; guard_target =ₛ x = 1#32; assumption
+example (h : x = (4 : Std.BitVec 32)) : x = udiv 9 2 := by
+  simp; guard_target =ₛ x = 4#32; assumption
+example (h : x = (1 : Std.BitVec 32)) : x = umod 9 2 := by
+  simp; guard_target =ₛ x = 1#32; assumption
+example (h : x = (4 : Std.BitVec 32)) : x = sdiv (-9) (-2) := by
+  simp; guard_target =ₛ x = 4#32; assumption
+example (h : x = (1 : Std.BitVec 32)) : x = smod (-9) 2 := by
+  simp; guard_target =ₛ x = 1#32; assumption
+example (h : x = (1 : Std.BitVec 32)) : x = - smtUDiv 9 0 := by
+  simp; guard_target =ₛ x = 1#32; assumption
+example (h : x = (1 : Std.BitVec 32)) : x = - srem (-9) 2 := by
+  simp; guard_target =ₛ x = 1#32; assumption
+example (h : x = (1 : Std.BitVec 32)) : x = - smtSDiv 9 0 := by
+  simp; guard_target =ₛ x = 1#32; assumption
+example (h : x = (1 : Std.BitVec 32)) : x = smtSDiv (-9) 0 := by
+  simp; guard_target =ₛ x = 1#32; assumption
+example (h : x = false) : x = (4#3).getLsb 0:= by
+  simp; guard_target =ₛ x = false; assumption
+example (h : x = true) : x = (4#3).getLsb 2:= by
+  simp; guard_target =ₛ x = true; assumption
+example (h : x = true) : x = (4#3).getMsb 0:= by
+  simp; guard_target =ₛ x = true; assumption
+example (h : x = false) : x = (4#3).getMsb 2:= by
+  simp; guard_target =ₛ x = false; assumption
+example (h : x = (24 : Std.BitVec 32)) : x = 6#32 <<< 2 := by
+  simp; guard_target =ₛ x = 24#32; assumption
+example (h : x = (1 : Std.BitVec 32)) : x = 6#32 >>> 2 := by
+  simp; guard_target =ₛ x = 1#32; assumption
+example (h : x = (24 : Std.BitVec 32)) : x = BitVec.shiftLeft 6#32 2 := by
+  simp; guard_target =ₛ x = 24#32; assumption
+example (h : x = (1 : Std.BitVec 32)) : x = BitVec.ushiftRight 6#32 2 := by
+  simp; guard_target =ₛ x = 1#32; assumption
+example (h : x = (2 : Std.BitVec 32)) : x = - BitVec.sshiftRight (- 6#32) 2 := by
+  simp; guard_target =ₛ x = 2#32; assumption
+example (h : x = (5 : Std.BitVec 3)) : x = BitVec.rotateLeft (6#3) 1 := by
+  simp; guard_target =ₛ x = 5#3; assumption
+example (h : x = (3 : Std.BitVec 3)) : x = BitVec.rotateRight (6#3) 1 := by
+  simp; guard_target =ₛ x = 3#3; assumption
+example (h : x = (7 : Std.BitVec 5)) : x = 1#3 ++ 3#2 := by
+  simp; guard_target =ₛ x = 7#5; assumption
+example (h : x = (1 : Std.BitVec 3)) : x = BitVec.cast (by decide : 3=2+1) 1#3 := by
+  simp; guard_target =ₛ x = 1#3; assumption
+example (h : x = 5) : x = (2#3 + 3#3).toNat := by
+  simp; guard_target =ₛ x = 5; assumption
+example (h : x = -1) : x = (2#3 - 3#3).toInt := by
+  simp; guard_target =ₛ x = -1; assumption
+example (h : x = (1 : Std.BitVec 3)) : x = -BitVec.ofInt 3 (-1) := by
+  simp; guard_target =ₛ x = 1#3; assumption
+example (h : x) : x = (1#3 < 3#3) := by
+  simp; guard_target =ₛ x; assumption
+example (h : x) : x = (BitVec.ult 1#3 3#3) := by
+  simp; guard_target =ₛ x; assumption
+example (h : ¬x) : x = (4#3 < 3#3) := by
+  simp; guard_target =ₛ ¬x; assumption
+example (h : x) : x = (BitVec.slt (- 4#3) 3#3) := by
+  simp; guard_target =ₛ x; assumption
+example (h : x) : x = (BitVec.sle (- 4#3) 3#3) := by
+  simp; guard_target =ₛ x; assumption
+example (h : x) : x = (3#3 > 1#3) := by
+  simp; guard_target =ₛ x; assumption
+example (h : ¬x) : x = (3#3 > 4#3) := by
+  simp; guard_target =ₛ ¬x; assumption
+example (h : x) : x = (1#3 ≤ 3#3) := by
+  simp; guard_target =ₛ x; assumption
+example (h : ¬x) : x = (4#3 ≤ 3#3) := by
+  simp; guard_target =ₛ ¬x; assumption
+example (h : ¬x) : x = (BitVec.ule 4#3 3#3) := by
+  simp; guard_target =ₛ ¬x; assumption
+example (h : x) : x = (3#3 ≥ 1#3) := by
+  simp; guard_target =ₛ x; assumption
+example (h : ¬x) : x = (3#3 ≥ 4#3) := by
+  simp; guard_target =ₛ ¬x; assumption
+example (h : x = (5 : Std.BitVec 7)) : x = (5#3).zeroExtend' (by decide) := by
+  simp; guard_target =ₛ x = 5#7; assumption
+example (h : x = (80 : Std.BitVec 7)) : x = (5#3).shiftLeftZeroExtend 4 := by
+  simp; guard_target =ₛ x = 80#7; assumption
+example (h : x = (5: Std.BitVec 3)) : x = (10#5).extractLsb' 1 3 := by
+  simp; guard_target =ₛ x = 5#3; assumption
+example (h : x = (9: Std.BitVec 6)) : x = (1#3).replicate 2 := by
+  simp; guard_target =ₛ x = 9#6; assumption
+example (h : x = (5 : Std.BitVec 7)) : x = (5#3).zeroExtend 7 := by
+  simp; guard_target =ₛ x = 5#7; assumption