feat(PBV): Convert multiplication of masks into shifts of popcounts.

UnitTest/BoundedBitblasting/CounterExamples.lean

@@ -17,6 +17,7 @@ error: The prover found a counterexample, consider the following assignment:
 m_w1 = 255#8
 m_w2 = 0#8
 m_w0 = 127#8
+m_lit8 = 255#8
 x = 127#8
 -/
 #guard_msgs in
@@ -65,8 +66,8 @@ error: `pbv_decide` found a counterexample, consider the following assignment:
   w + v = 8  	(m_w0_add_w1 = 0xff#8)
   v = 4  	(m_w1 = 0x0f#8)
   v + w = 8  	(m_w1_add_w0 = 0xff#8)
-  x = 0xe#4
-  y = 0xf#4
+  x = 0xf#4
+  y = 0xe#4
 -/
 #guard_msgs in
 example (v w : Nat) (x : BitVec v) (y : BitVec w) (hv : v ≤ 4) (hw : w ≤ 4) (h : v = w) :
@@ -126,8 +127,8 @@ error: `pbv_decide` found a potentially spurious counterexample.
   The following expressions were abstracted as opaque variables:
     - BitVec.ofBool (BitVec.setWidth w x + 1#w == BitVec.setWidth w x) = 0x1#1
 Consider the following assignment:
-  w = 0  	(m_w0 = 0x0#4)
-  x = 0x0#0
+  w = 4  	(m_w0 = 0xf#4)
+  x = 0xf#4
 -/
 #guard_msgs in
 example (w : Nat) (x : BitVec w) (hw : w ≤ 4) :

Veir/Data/PBV/Examples.lean

@@ -238,7 +238,7 @@ theorem trace_append (w : Nat) (a b : BitVec w) (hw : w ≤ 8) :
   intro b h_bmw
 -- Step 5: Convert width hypothesis to mask hypothesis.
   have mw_mask := and_add_one_eq_zero_of_maskOfWidth h_mw
-  have w_add_w_mask := add_eq_mul_of_maskOfWidth w_le_bw w_le_bw w_add_w_le_bw h_mw h_mw h_mw_add_w
+  have w_add_w_mask := add_eq_shift_sum_of_maskOfWidth w_le_bw w_le_bw w_add_w_le_bw h_mw h_mw h_mw_add_w
 -- Step 5B: Translate the width precondition `w ≤ 8` into `mw ≤ BitVec.ofNat 16 (2 ^ 8 - 1)`
   let lit8 : BitVec 16 := 255#16
   have h_lit8_mask : lit8 = maskOfWidth 16 8 := by rfl

Veir/Data/PBV/Mask.lean

@@ -64,6 +64,25 @@ theorem maskOfWidth_eq_twoPow_sub_one {o w : Nat} (h : w ≤ o) :
   apply BitVec.eq_of_toNat_eq
   grind [maskOfWidth_add_one_eq_twoPow]
 
+/-- A mask is an `allOnes` zero-extended to `o`. -/
+theorem maskOfWidth_eq_allOnes {o w : Nat} (h : w ≤ o) : maskOfWidth o w = BitVec.zeroExtend o (BitVec.allOnes w)
+  := by
+  apply BitVec.eq_of_toNat_eq
+  simp only [toNat_maskOfWidth h, BitVec.truncate_eq_setWidth, BitVec.toNat_setWidth, BitVec.toNat_allOnes]
+  rw [Nat.mod_eq_of_lt (by grind [Nat.pow_le_pow_right (n := 2) (by lia) h])]
+
+/-- The popcount of a mask is the value of the mask width. -/
+theorem toNat_cpop_maskOfWidth_eq_width {o w : Nat} (h : w ≤ o) : (BitVec.cpop (maskOfWidth o w)).toNat = w
+  := by
+  simp only [maskOfWidth_eq_allOnes h, BitVec.truncate_eq_setWidth, BitVec.toNat_cpop_setWidth_eq_of_le h,
+    BitVec.cpop_allOnes, BitVec.toNat_ofNat, Nat.mod_two_pow_self]
+
+/-- Push a variable `Nat` which corresponds to a mask into a `cpop` of the mask. -/
+theorem cpop_eq_width_of_maskOfWidth {o w : Nat} {m : BitVec o} (h : w ≤ o) (hm : m = maskOfWidth o w) : m.cpop = BitVec.ofNat o w := by
+  apply BitVec.eq_of_toNat_eq
+  simp only [hm, toNat_cpop_maskOfWidth_eq_width h, BitVec.toNat_ofNat]
+  rw [Nat.mod_eq_of_lt (by grind [Nat.lt_pow_self])]
+
 /-- Every mask of blast width `0` is the empty bitvector. -/
 @[simp] theorem maskOfWidth_zero_eq_zero {w : Nat} : maskOfWidth 0 w = 0#0 := by
   apply BitVec.eq_of_toNat_eq
@@ -117,17 +136,15 @@ theorem le_of_le_of_eq_maskOfWidth {o w₁ w₂ : Nat} {m₁ m₂ : BitVec o} (h
 
 /-- Adding widths becomes multiplying masks: the mask `m₃` of `w₁ + w₂` is
 `2^w₁ * 2^w₂ - 1`, written in terms of the masks `m₁` and `m₂`. -/
-theorem add_eq_mul_of_maskOfWidth {o w₁ w₂ : Nat} {m₁ m₂ m₃ : BitVec o}
+theorem add_eq_shift_sum_of_maskOfWidth {o w₁ w₂ : Nat} {m₁ m₂ m₃ : BitVec o}
     (h₁ : w₁ ≤ o) (h₂ : w₂ ≤ o) (h₁₂ : w₁ + w₂ ≤ o)
     (hm₁ : m₁ = maskOfWidth o w₁) (hm₂ : m₂ = maskOfWidth o w₂)
     (hm₃ : m₃ = maskOfWidth o (w₁ + w₂)) :
-    m₃ = (m₁ + 1#o) * (m₂ + 1#o) - 1#o := by
+    m₃ = (1#o <<< (BitVec.cpop m₁ + BitVec.cpop m₂)) - 1#o := by
   subst m₃
-  cases o
-  · simp [hm₁, hm₂, maskOfWidth_zero_eq_zero]
-  · rw [hm₁, maskOfWidth_add_one_eq_twoPow h₁, hm₂, maskOfWidth_add_one_eq_twoPow h₂,
-      BitVec.twoPow_mul_twoPow_eq]
-    apply maskOfWidth_eq_twoPow_sub_one h₁₂
+  rw [cpop_eq_width_of_maskOfWidth h₁ hm₁, cpop_eq_width_of_maskOfWidth h₂ hm₂,
+      BitVec.ofNat_add_ofNat, BitVec.shiftLeft_ofNat_eq, BitVec.shiftLeft_eq_mul_twoPow,
+      BitVec.one_mul, Nat.mod_eq_of_lt (by grind[Nat.lt_pow_self]), maskOfWidth_eq_twoPow_sub_one h₁₂]
 
 /-! ## The sign bit helpers -/
 

Veir/Data/PBV/Push.lean

@@ -73,14 +73,13 @@ longer overlap, so they can be recombined with `|||`. -/
 theorem setWidth_append_eq_or_mul_maskOfWidth_add_one {w o : Nat} (h : w ≤ o) :
     ∀ {v : Nat} (a : BitVec v) (b : BitVec w), v + w ≤ o →
       (a ++ b).setWidth o
-        = ((a.setWidth o) * (maskOfWidth o w + 1#o)) ||| b.setWidth o := by
+        = ((a.setWidth o) <<< BitVec.cpop (maskOfWidth o w)) ||| b.setWidth o := by
   intro v a b hvw
   apply BitVec.eq_of_toNat_eq
   simp only [BitVec.toNat_or, BitVec.toNat_setWidth_of_le, hvw, h,
-      BitVec.toNat_append, maskOfWidth_add_one_eq_twoPow h,
-      BitVec.mul_twoPow_eq_shiftLeft, BitVec.toNat_shiftLeft]
+      BitVec.toNat_append, BitVec.shiftLeft_eq', BitVec.toNat_shiftLeft]
   congr 1
-  rw [Nat.shiftLeft_eq, Nat.shiftLeft_eq, BitVec.toNat_setWidth_of_le (by lia), Nat.mod_eq_of_lt]
+  rw [toNat_cpop_maskOfWidth_eq_width h, BitVec.toNat_setWidth_of_le (by lia), Nat.mod_eq_of_lt]
   have a_lt_vw := Nat.mul_lt_mul_of_lt_of_le a.isLt (Nat.le_refl _) (Nat.two_pow_pos w)
   grind [Nat.pow_le_pow_right (n := 2) (by lia) hvw]
 

Veir/Meta/Tactic/PBVDecide/Main.lean

@@ -304,14 +304,17 @@ meta def introMaskLit (g : MVarId) (widthLit : Tm .width) (infos : WidthInfos) :
   let lit ← mkAppM ``BitVec.ofNat #[o, mkNatLit (2 ^ val - 1)]
   let maskTy ← mkAppM ``BitVec #[o]
   -- Define the mask
-  let g ← g.define (Name.mkSimple s!"m_{widthLit.toName}") maskTy lit
+  let maskName := Name.mkSimple s!"m_{widthLit.toName}"
+  let g ← g.assertExt maskName maskTy lit
   let (mask, g) ← g.intro1P
+  let (_maskValue, g) ← g.introN 1 [Name.mkSimple s!"{maskName}_val"]
   -- Prove that the mask is indeed a maskOfWidth
   let applyMask ← mkAppM ``maskOfWidth #[o, n]
   let proof ← g.withContext do mkExpectedTypeHint (← mkEqRefl (mkFVar mask)) (← mkEq (mkFVar mask) applyMask)
   let (maskHyp, g) ← g.withContext do g.note (Name.mkSimple s!"h_m_{widthLit.toName}") proof
   -- Prove that the lit respects the bound
-  let (hypWidthLeBound, g) ← g.note (Name.mkSimple s!"h_m_{widthLit.toName}_le_blast") <| ← mkDecideProof (mkNatLE n o)
+  let (hypWidthLeBound, g) ← g.withContext do
+    g.note (Name.mkSimple s!"h_m_{widthLit.toName}_le_blast") <| ← mkDecideProof (mkNatLE n o)
 
   let info : WidthInfo := {
     widthTm := widthLit,
@@ -343,9 +346,9 @@ meta def getOrCreateWidthMask (g : MVarId) (widthTm : Tm .width) (infos : WidthI
     let (g, wInfo, infos) ← getOrCreateWidthMask g w infos
     -- Intro the mask for this term
     let (g, thisInfo, infos) ← introMaskWidth g widthTm infos
-    -- Rewrite the mask of a sum of widths into a product of the masks (+ 1).
+    -- Rewrite the mask of a sum of widths in terms of the underlying masks.
     let (_hyp, g) ← g.withContext do
-      g.note (Name.mkSimple s!"bv_{widthTm.toName}") <| ← mkAppM ``add_eq_mul_of_maskOfWidth #[
+      g.note (Name.mkSimple s!"bv_{widthTm.toName}") <| ← mkAppM ``add_eq_shift_sum_of_maskOfWidth #[
         .fvar vInfo.hypWidthLeBoundNote,
         .fvar wInfo.hypWidthLeBoundNote,
         .fvar thisInfo.hypWidthLeBoundNote,
@@ -709,33 +712,26 @@ meta structure WidthMaskCex where
   counterExample : Expr × BVExpr.PackedBitVec
   /-- Width expression the mask encodes. -/
   widthNatExpr : Expr
+  /-- Width term this mask corresponds to. -/
+  widthTm : Tm .width
   /-- User facing name of the mask. -/
   name : Name
 
 /-- Value of the width, derived from the bitvector. -/
-meta def WidthMaskCex.widthVal (self : WidthMaskCex) : Nat :=
+meta def WidthMaskCex.val (self : WidthMaskCex) : Nat :=
   BitVec.cpop self.counterExample.snd.bv |> BitVec.toNat
 
 abbrev WidthMaskCexs := HashMap Name WidthMaskCex
 
 meta instance : ToMessageData WidthMaskCex where
-  toMessageData f := m!"{f.widthNatExpr} = {f.widthVal}  \t({f.name} = {f.counterExample.snd.bv})"
-
-/-- Concrete width is either a literal or a counterexample. -/
-meta inductive ConcreteWidth where
-  | lit : Nat -> ConcreteWidth
-  | cex : WidthMaskCex -> ConcreteWidth
-
-meta def ConcreteWidth.val : ConcreteWidth -> Nat
-  | .lit val => val
-  | .cex widthCex => widthCex.widthVal
+  toMessageData f := m!"{f.widthNatExpr} = {f.val}  \t({f.name} = {f.counterExample.snd.bv})"
 
 /-- BitVec counterexample to hold information to be displayed. -/
 meta structure BitVecCex where
   /-- Original counterexample. -/
   counterExample : Expr × BVExpr.PackedBitVec
   /-- Corresponding concrete width. -/
-  width : ConcreteWidth
+  width : WidthMaskCex
   /-- User facing variable name. -/
   name : Name
 
@@ -774,14 +770,12 @@ meta def getWidthCounterExamples (widthInfos : WidthInfos) (counterExample : Cou
       let username ← counterExample.goal.withContext do eq.fvarId!.getUserName
       widthMaskCexs := widthMaskCexs.insert name {
           counterExample := (eq, bv),
-          widthNatExpr := originalNatWidth, name := username
+          widthNatExpr := originalNatWidth,
+          name := username,
+          widthTm := winfo.widthTm
       }
     | none =>
-      if let .widthLit _ := winfo.widthTm then
-        -- masks of width literals are assigned by definition
-        pure ()
-      else
-        logWarning m!"No assignment found in the counterexample for mask {name} of width {originalNatWidth}."
+      logWarning m!"No assignment found in the counterexample for mask {name} of width {originalNatWidth}."
 
   return widthMaskCexs
 
@@ -794,12 +788,9 @@ meta def getBitVecCounterExamples (bvInfos : BitVecInfos) (widthCexs: WidthMaskC
     let name ← bvinfo.bvVar.getUserName
     match findFVarIdInCounterExample? counterExample bvinfo.bvVar with
     | some (eq, bv) => do
-      if let .widthLit val := bvinfo.bvWidthTm then
-        return {counterExample := (eq, bv), width := .lit val, name}
-      else
-        let some widthCex := widthCexs[bvinfo.bvWidthTm.toName]?
-          | throwError m!"Width ({bvinfo.bvWidthTm.toName}) of BitVec {name} is missing from the generated counterexamples."
-        return {counterExample := (eq, bv), width := .cex widthCex, name}
+      let some widthCex := widthCexs[bvinfo.bvWidthTm.toName]?
+        | throwError m!"Width ({bvinfo.bvWidthTm.toName}) of BitVec {name} is missing from the generated counterexamples."
+      return {counterExample := (eq, bv), width := widthCex, name}
     | none =>
       throwError m!"No counterexample generated for BitVec {name}"
   )
@@ -838,7 +829,7 @@ meta def prettyPrintCounterExample (counterExample : CounterExample) (widthInfos
   let widthCexsA := widthCexs.toArray.map (·.snd) |>.qsort (fun a b => Name.lt a.name b.name)
   let bitvecCexs := bitvecCexs.qsort (fun a b => Name.lt a.name b.name)
 
-  err := widthCexsA.foldl (init := err) (fun acc cex => acc ++ m!"  {cex}\n")
+  err := widthCexsA.foldl (init := err) (fun acc cex => if let .widthLit _ := cex.widthTm then acc else acc ++ m!"  {cex}\n")
   err := bitvecCexs.foldl (init := err) (fun acc cex => acc ++ m!"  {cex}\n")
 
   return err