feat: BitVec.replicate

LeanSAT/BitBlast/BVExpr/Basic.lean

@@ -208,6 +208,7 @@ A unary operation on two `BVExpr`.
 Concatenate two bit vectors
 -/
 | append (lhs : BVExpr l) (rhs : BVExpr r) : BVExpr (l + r)
+| replicate (n : Nat) (expr : BVExpr w) : BVExpr (w * n)
 /--
 sign extend a `BitVec` by some constant amount.
 -/
@@ -231,6 +232,7 @@ def toString : BVExpr w → String
   | .bin lhs op rhs => s!"({lhs.toString} {op.toString} {rhs.toString})"
   | .un op operand => s!"({op.toString} {toString operand})"
   | .append lhs rhs => s!"({toString lhs} ++ {toString rhs})"
+  | .replicate n expr => s!"(replicate {n} {toString expr})"
   | .signExtend v expr => s!"(sext {v} {expr.toString})"
   | .shiftLeft lhs rhs => s!"({lhs.toString} << {rhs.toString})"
   | .shiftRight lhs rhs => s!"({lhs.toString} >> {rhs.toString})"
@@ -269,6 +271,7 @@ def eval (assign : Assignment) : BVExpr w → BitVec w
   | .bin lhs op rhs => op.eval (eval assign lhs) (eval assign rhs)
   | .un op operand => op.eval (eval assign operand)
   | .append lhs rhs => (eval assign lhs) ++ (eval assign rhs)
+  | .replicate n expr => BitVec.replicate n (eval assign expr)
   | .signExtend v expr => BitVec.signExtend v (eval assign expr)
   | .shiftLeft lhs rhs => (eval assign lhs) <<< (eval assign rhs)
   | .shiftRight lhs rhs => (eval assign lhs) >>> (eval assign rhs)
@@ -300,6 +303,10 @@ theorem eval_un : eval assign (.un op operand) = op.eval (operand.eval assign) :
 theorem eval_append : eval assign (.append lhs rhs) = (lhs.eval assign) ++ (rhs.eval assign) := by
   rfl
 
+@[simp]
+theorem eval_replicate : eval assign (.replicate n expr) = BitVec.replicate n (expr.eval assign) := by
+  rfl
+
 @[simp]
 theorem eval_signExtend : eval assign (.signExtend v expr) = BitVec.signExtend v (eval assign expr) := by
   rfl

LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Expr.lean

@@ -11,6 +11,7 @@ import LeanSAT.BitBlast.BVExpr.BitBlast.Impl.ShiftRight
 import LeanSAT.BitBlast.BVExpr.BitBlast.Impl.Add
 import LeanSAT.BitBlast.BVExpr.BitBlast.Impl.ZeroExtend
 import LeanSAT.BitBlast.BVExpr.BitBlast.Impl.Append
+import LeanSAT.BitBlast.BVExpr.BitBlast.Impl.Replicate
 import LeanSAT.BitBlast.BVExpr.BitBlast.Impl.Extract
 import LeanSAT.BitBlast.BVExpr.BitBlast.Impl.RotateLeft
 import LeanSAT.BitBlast.BVExpr.BitBlast.Impl.RotateRight
@@ -182,6 +183,16 @@ where
           dsimp at hlaig hraig
           omega
       ⟩
+    | .replicate n expr =>
+      let ⟨⟨aig, expr⟩, haig⟩ := go aig expr
+      let res := bitblast.blastReplicate aig ⟨n, expr, rfl⟩
+      ⟨
+        res,
+        by
+          apply AIG.LawfulStreamOperator.le_size_of_le_aig_size (f := bitblast.blastReplicate)
+          dsimp at haig
+          assumption
+      ⟩
     | .extract hi lo expr =>
       let ⟨⟨eaig, estream⟩, heaig⟩ := go aig expr
       let res := bitblast.blastExtract eaig ⟨estream, hi, lo, rfl⟩
@@ -288,6 +299,13 @@ theorem bitblast.go_decl_eq (aig : AIG BVBit) (expr : BVExpr w)
       . apply Nat.le_trans
         . exact (bitblast.go aig lhs).property
         . exact (go (go aig lhs).1.aig rhs).property
+  | replicate n inner ih =>
+    dsimp [go]
+    rw [AIG.LawfulStreamOperator.decl_eq (f := blastReplicate)]
+    rw [ih]
+    apply Nat.lt_of_lt_of_le
+    . exact h1
+    . exact (go aig inner).property
   | extract hi lo inner ih =>
     dsimp [go]
     rw [AIG.LawfulStreamOperator.decl_eq (f := blastExtract)]

LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Replicate.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import LeanSAT.BitBlast.BVExpr.Basic
+import LeanSAT.AIG.LawfulStreamOperator
+
+namespace BVExpr
+namespace bitblast
+
+variable [Hashable α] [DecidableEq α]
+
+structure ReplicateTarget (aig : AIG α) (combined : Nat) where
+  {w : Nat}
+  n : Nat
+  inner : AIG.RefStream aig w
+  h : combined = w * n
+
+def blastReplicate (aig : AIG α) (target : ReplicateTarget aig newWidth)
+    : AIG.RefStreamEntry α newWidth :=
+  let ⟨n, inner, h⟩ := target
+  let ref := go n 0 (by omega) inner .empty
+  ⟨aig, h ▸ ref⟩
+where
+  go {aig : AIG α} {w : Nat} (n : Nat) (curr : Nat) (hcurr : curr ≤ n) (input : AIG.RefStream aig w)
+      (s : AIG.RefStream aig (w * curr)) : AIG.RefStream aig (w * n) :=
+    if h : curr < n then
+      let s := s.append input
+      go n (curr + 1) (by omega) input s
+    else
+      have : curr = n := by omega
+      this ▸ s
+  termination_by n - curr
+
+instance : AIG.LawfulStreamOperator α ReplicateTarget blastReplicate where
+  le_size := by simp [blastReplicate]
+  decl_eq := by simp [blastReplicate]
+
+end bitblast
+end BVExpr

LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean

@@ -12,6 +12,7 @@ import LeanSAT.BitBlast.BVExpr.BitBlast.Lemmas.ShiftRight
 import LeanSAT.BitBlast.BVExpr.BitBlast.Lemmas.Add
 import LeanSAT.BitBlast.BVExpr.BitBlast.Lemmas.ZeroExtend
 import LeanSAT.BitBlast.BVExpr.BitBlast.Lemmas.Append
+import LeanSAT.BitBlast.BVExpr.BitBlast.Lemmas.Replicate
 import LeanSAT.BitBlast.BVExpr.BitBlast.Lemmas.Extract
 import LeanSAT.BitBlast.BVExpr.BitBlast.Lemmas.RotateLeft
 import LeanSAT.BitBlast.BVExpr.BitBlast.Lemmas.RotateRight
@@ -71,6 +72,7 @@ theorem go_denote_eq_eval_getLsb (aig : AIG BVBit) (expr : BVExpr w) (assign : A
     . next hsplit =>
       simp only [hsplit, decide_False, cond_false]
       rw [go_denote_mem_prefix, lih]
+  | replicate n expr ih => simp [go, ih, hidx]
   | signExtend v inner ih =>
     rename_i originalWidth
     generalize hgo : (go aig (signExtend v inner)).val = res

LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Replicate.lean

@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import LeanSAT.BitBlast.BVExpr.BitBlast.Lemmas.Basic
+import LeanSAT.BitBlast.BVExpr.BitBlast.Impl.Replicate
+
+open AIG
+
+namespace BVExpr
+namespace bitblast
+
+variable [Hashable α] [DecidableEq α]
+
+namespace blastReplicate
+
+private theorem aux1 {a b c : Nat} (h : b < a * c) : 0 < a := by
+  by_cases a = 0
+  · simp_all
+  · omega
+
+private theorem aux2 {a b c : Nat} (hidx1 : b < c * a) : b % c < c := by
+  apply Nat.mod_lt
+  apply aux1
+  assumption
+
+private theorem aux3 {a b c : Nat} (hidx : a < b * c) (h : c < n) : a < b * n := by
+  apply Nat.lt_trans
+  · exact hidx
+  · apply (Nat.mul_lt_mul_left _).mpr h
+    apply aux1
+    assumption
+
+private theorem aux4 {a b c : Nat} (hidx : a < b * c) (h : c ≤ n) : a < b * n := by
+  cases Nat.lt_or_eq_of_le h with
+  | inl h => apply aux3 <;> assumption
+  | inr h => simp_all
+
+theorem go_getRef_aux (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n)
+    (input : AIG.RefStream aig w) (s : AIG.RefStream aig (w * curr))
+    : ∀ (idx : Nat) (hidx : idx < w * curr),
+        (go n curr hcurr input s).getRef idx (aux4 hidx hcurr)
+          =
+        s.getRef idx hidx := by
+  intro idx hidx
+  unfold go
+  split
+  . dsimp
+    rw [go_getRef_aux]
+    rw [AIG.RefStream.getRef_append]
+    simp only [hidx, ↓reduceDIte]
+    omega
+  . dsimp
+    simp only [RefStream.getRef, Ref.mk.injEq]
+    have : curr = n := by omega
+    subst this
+    simp
+termination_by n - curr
+
+theorem go_getRef (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n)
+    (input : AIG.RefStream aig w) (s : AIG.RefStream aig (w * curr))
+  : ∀ (idx : Nat) (hidx1 : idx < w * n),
+      w * curr ≤ idx
+        →
+      (go n curr hcurr input s).getRef idx hidx1
+        =
+      input.getRef (idx % w) (aux2 hidx1) := by
+  intro idx hidx1 hidx2
+  unfold go
+  dsimp
+  split
+  . cases Nat.lt_or_ge idx (w * (curr + 1)) with
+    | inl h =>
+      rw [go_getRef_aux]
+      rw [AIG.RefStream.getRef_append]
+      . have : ¬ (idx < w * curr) := by omega
+        simp only [this, ↓reduceDIte]
+        congr 1
+        rw [← Nat.sub_mul_mod (k := curr)]
+        . rw [Nat.mod_eq_of_lt]
+          apply Nat.sub_lt_left_of_lt_add <;> assumption
+        . assumption
+      . simpa using h
+    | inr h =>
+      rw [go_getRef]
+      assumption
+  . have : curr = n := by omega
+    rw [this] at hidx2
+    omega
+termination_by n - curr
+
+end blastReplicate
+
+@[simp]
+theorem blastReplicate_eq_eval_getLsb (aig : AIG α) (target : ReplicateTarget aig newWidth)
+    (assign : α → Bool)
+  : ∀ (idx : Nat) (hidx : idx < newWidth),
+      ⟦
+        (blastReplicate aig target).aig,
+        (blastReplicate aig target).stream.getRef idx hidx,
+        assign
+      ⟧
+        =
+      ⟦
+        aig,
+        target.inner.getRef (idx % target.w) (blastReplicate.aux2 (target.h ▸ hidx)),
+        assign
+      ⟧ := by
+  intro idx hidx
+  rcases target with ⟨n, input, h⟩
+  unfold blastReplicate
+  dsimp
+  subst h
+  rw [blastReplicate.go_getRef]
+  omega

LeanSAT/Tactics/BVDecide.lean

@@ -62,6 +62,8 @@ where
   | .un op operand => mkApp3 (mkConst ``BVExpr.un) (toExpr w) (toExpr op) (go operand)
   | .append (l := l) (r := r) lhs rhs =>
     mkApp4 (mkConst ``BVExpr.append) (toExpr l) (toExpr r) (go lhs) (go rhs)
+  | .replicate (w := oldWidth) w inner =>
+    mkApp3 (mkConst ``BVExpr.replicate) (toExpr oldWidth) (toExpr w) (go inner)
   | .extract (w := oldWidth) hi lo expr =>
     mkApp4 (mkConst ``BVExpr.extract) (toExpr oldWidth) (toExpr hi) (toExpr lo) (go expr)
   | .shiftLeft (m := m) (n := n) lhs rhs =>
@@ -248,6 +250,10 @@ theorem append_congr (lw rw : Nat) (lhs lhs' : BitVec lw) (rhs rhs' : BitVec rw)
     lhs' ++ rhs' = lhs ++ rhs := by
   simp[*]
 
+theorem replicate_congr (n : Nat) (w : Nat) (expr expr' : BitVec w) (h : expr' = expr) :
+    BitVec.replicate n expr' = BitVec.replicate n expr := by
+  simp[*]
+
 theorem extract_congr (hi lo : Nat) (w : Nat) (x x' : BitVec w) (h1 : x = x') :
     BitVec.extractLsb hi lo x' = BitVec.extractLsb hi lo x := by
   simp[*]
@@ -394,6 +400,24 @@ partial def of (x : Expr) : M (Option ReifiedBVExpr) := do
         rhsExpr rhsEval
         lhsProof rhsProof
     return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩
+  | BitVec.replicate _ nExpr innerExpr =>
+    let some inner ← ofOrAtom innerExpr | return none
+    let some n ← getNatValue? nExpr | return ← ofAtom x
+    let bvExpr := .replicate n inner.bvExpr
+    let expr := mkApp3 (mkConst ``BVExpr.replicate)
+      (toExpr inner.width)
+      (toExpr n)
+      inner.expr
+    let proof := do
+      let innerEval ← mkEvalExpr inner.width inner.expr
+      let innerProof ← inner.evalsAtAtoms
+      return mkApp5 (mkConst ``replicate_congr)
+        (toExpr n)
+        (toExpr inner.width)
+        innerExpr
+        innerEval
+        innerProof
+    return some ⟨inner.width * n, bvExpr, proof, expr⟩
   | BitVec.extractLsb _ hiExpr loExpr innerExpr =>
     let some hi ← getNatValue? hiExpr | return ← ofAtom x
     let some lo ← getNatValue? loExpr | return ← ofAtom x

LeanSAT/Tactics/Normalize/BitVec.lean

@@ -213,6 +213,8 @@ theorem BitVec.max_ult' (a : BitVec w) : (BitVec.ult (-1#w) a) = false := by
   rw [BitVec.lt_ult] at this
   simp [this]
 
+attribute [bv_normalize] BitVec.replicate_zero_eq
+
 end Normalize
 end BVDecide
 

Test/Bv/Cast.lean

@@ -41,3 +41,11 @@ theorem cast_unit_7 (x : BitVec 64) : x.signExtend 128 = (x.signExtend 64).signE
 set_option trace.bv true in
 theorem cast_unit_8 (x : BitVec 64) : (x.signExtend 128 = x.zeroExtend 128) ↔ (x.msb = false) := by
   bv_decide
+
+set_option trace.bv true in
+theorem cast_unit_9 (x : BitVec 32) : (x.replicate 20).zeroExtend 32 = x := by
+  bv_decide
+
+set_option trace.bv true in
+theorem cast_unit_10 (x : BitVec 32) : (x.replicate 20).getLsb 40 = x.getLsb 8 := by
+  bv_decide

lean-toolchain

@@ -1,2 +1,2 @@
-leanprover/lean4:nightly-2024-08-01
+leanprover/lean4:nightly-2024-08-02