feat: verification of replicate

leanprover · Aug 2, 2024 · 1bdbda0 · 1bdbda0
1 parent eafed35
commit 1bdbda0
Show file tree

Hide file tree

Showing 3 changed files with 109 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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