From 12c8c407f587c3572c069e6548e1007114be2340 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 2 Aug 2024 09:03:58 +0200
Subject: [PATCH 1/5] feat: implement and integrate BitVec.replicate

---
 LeanSAT/BitBlast/BVExpr/Basic.lean            |  7 ++++
 .../BitBlast/BVExpr/BitBlast/Impl/Expr.lean   | 18 +++++++++
 .../BVExpr/BitBlast/Impl/Replicate.lean       | 40 +++++++++++++++++++
 .../BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean |  1 +
 .../BVExpr/BitBlast/Lemmas/Replicate.lean     | 10 +++++
 LeanSAT/Tactics/BVDecide.lean                 | 24 +++++++++++
 6 files changed, 100 insertions(+)
 create mode 100644 LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Replicate.lean
 create mode 100644 LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Replicate.lean

diff --git a/LeanSAT/BitBlast/BVExpr/Basic.lean b/LeanSAT/BitBlast/BVExpr/Basic.lean
index 049a247c..4cb562d3 100644
--- a/LeanSAT/BitBlast/BVExpr/Basic.lean
+++ b/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
diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Expr.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Expr.lean
index 22a8c949..ebd09b1d 100644
--- a/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Expr.lean
+++ b/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)]
diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Replicate.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Replicate.lean
new file mode 100644
index 00000000..b5f0e15f
--- /dev/null
+++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Replicate.lean
@@ -0,0 +1,40 @@
+/-
+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
+
+instance : AIG.LawfulStreamOperator α ReplicateTarget blastReplicate where
+  le_size := by simp [blastReplicate]
+  decl_eq := by simp [blastReplicate]
+
+end bitblast
+end BVExpr
diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean
index 35172d62..e93df106 100644
--- a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean
+++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean
@@ -71,6 +71,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 => sorry
   | signExtend v inner ih =>
     rename_i originalWidth
     generalize hgo : (go aig (signExtend v inner)).val = res
diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Replicate.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Replicate.lean
new file mode 100644
index 00000000..08169209
--- /dev/null
+++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Replicate.lean
@@ -0,0 +1,10 @@
+/-
+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
+
diff --git a/LeanSAT/Tactics/BVDecide.lean b/LeanSAT/Tactics/BVDecide.lean
index 4ed15342..48706f7e 100644
--- a/LeanSAT/Tactics/BVDecide.lean
+++ b/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

From 0284bb37c13920e1916f73ed872c6963f71ffd08 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 2 Aug 2024 09:04:14 +0200
Subject: [PATCH 2/5] test: BitVec.replicate

---
 Test/Bv/Cast.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Test/Bv/Cast.lean b/Test/Bv/Cast.lean
index 53d6764e..491e6272 100644
--- a/Test/Bv/Cast.lean
+++ b/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

From cbd897a29dc88ba32d156bdefb29d8b2aa90f56d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 2 Aug 2024 10:54:58 +0200
Subject: [PATCH 3/5] chore: update toolchain

---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index f369dc35..dcbb9bc9 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1,2 +1,2 @@
-leanprover/lean4:nightly-2024-08-01
+leanprover/lean4:nightly-2024-08-02
 

From eafed35d9b2388ce6560d920473d386ad29e6cae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 2 Aug 2024 10:55:03 +0200
Subject: [PATCH 4/5] feat: simplify trivial BitVec.replicate

---
 LeanSAT/Tactics/Normalize/BitVec.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/LeanSAT/Tactics/Normalize/BitVec.lean b/LeanSAT/Tactics/Normalize/BitVec.lean
index 7798027d..adbc0182 100644
--- a/LeanSAT/Tactics/Normalize/BitVec.lean
+++ b/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
 

From 1bdbda0b77613f61732f03725525e6fc56c1ed1f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 2 Aug 2024 10:55:16 +0200
Subject: [PATCH 5/5] feat: verification of replicate

---
 .../BVExpr/BitBlast/Impl/Replicate.lean       |   1 +
 .../BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean |   3 +-
 .../BVExpr/BitBlast/Lemmas/Replicate.lean     | 106 ++++++++++++++++++
 3 files changed, 109 insertions(+), 1 deletion(-)

diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Replicate.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Replicate.lean
index b5f0e15f..be0cb24e 100644
--- a/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Replicate.lean
+++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Impl/Replicate.lean
@@ -31,6 +31,7 @@ where
     else
       have : curr = n := by omega
       this ▸ s
+  termination_by n - curr
 
 instance : AIG.LawfulStreamOperator α ReplicateTarget blastReplicate where
   le_size := by simp [blastReplicate]
diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean
index e93df106..fe536b2f 100644
--- a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Expr.lean
+++ b/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,7 +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 => sorry
+  | replicate n expr ih => simp [go, ih, hidx]
   | signExtend v inner ih =>
     rename_i originalWidth
     generalize hgo : (go aig (signExtend v inner)).val = res
diff --git a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Replicate.lean b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Replicate.lean
index 08169209..b7685f6a 100644
--- a/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Replicate.lean
+++ b/LeanSAT/BitBlast/BVExpr/BitBlast/Lemmas/Replicate.lean
@@ -8,3 +8,109 @@ 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