WIP: multiplication circuit for bit blasting

.github/ISSUE_TEMPLATE/bug_report.md

@@ -9,9 +9,15 @@ assignees: ''
 
 ### Prerequisites
 
-* [ ] Put an X between the brackets on this line if you have done all of the following:
-    * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues).
-    * Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
+Please put an X between the brackets as you perform the following steps:
+
+* [ ] Check that your issue is not already filed:
+      https://github.com/leanprover/lean4/issues
+* [ ] Reduce the issue to a minimal, self-contained, reproducible test case.
+      Avoid dependencies to Mathlib or Batteries.
+* [ ] Test your test case against the latest nightly release, for example on
+      https://live.lean-lang.org/#project=lean-nightly
+      (You can also use the settings there to switch to “Lean nightly”)
 
 ### Description
 
@@ -33,8 +39,8 @@ assignees: ''
 
 ### Versions
 
-[Output of `#eval Lean.versionString` or of `lean --version` in the folder that the issue occured in]
-[OS version]
+[Output of `#eval Lean.versionString`]
+[OS version, if not using live.lean-lang.org.]
 
 ### Additional Information
 

.github/workflows/pr-release.yml

@@ -126,11 +126,11 @@ jobs:
           if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
             echo "The merge base of this PR coincides with the nightly release"
 
-            STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
+            BATTERIES_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/batteries.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
             MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
 
-            if [[ -n "$STD_REMOTE_TAGS" ]]; then
-              echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+            if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
+              echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
               MESSAGE=""
 
               if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then
@@ -140,8 +140,8 @@ jobs:
                 MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
               fi
             else
-              echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
-              MESSAGE="- ❗ Std CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Std CI should run now."
+              echo "... but Batteries does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
+              MESSAGE="- ❗ Batteries CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Batteries CI should run now."
             fi
 
           else
@@ -151,7 +151,7 @@ jobs:
 
             git -C lean4.git fetch origin nightly-with-mathlib 
             NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "origin/nightly-with-mathlib")"
-            MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
+            MESSAGE="- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`."
           fi
 
           if [[ -n "$MESSAGE" ]]; then
@@ -223,35 +223,35 @@ jobs:
               description: description,
             });
 
-      # We next automatically create a Std branch using this toolchain.
-      # Std doesn't itself have a mechanism to report results of CI from this branch back to Lean
-      # Instead this is taken care of by Mathlib CI, which will fail if Std fails.
+      # We next automatically create a Batteries branch using this toolchain.
+      # Batteries doesn't itself have a mechanism to report results of CI from this branch back to Lean
+      # Instead this is taken care of by Mathlib CI, which will fail if Batteries fails.
       - name: Cleanup workspace
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         run: |
           sudo rm -rf ./*
 
-      # Checkout the Std repository with all branches
-      - name: Checkout Std repository
+      # Checkout the Batteries repository with all branches
+      - name: Checkout Batteries repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         uses: actions/checkout@v3
         with:
-          repository: leanprover/std4
+          repository: leanprover-community/batteries
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
 
       - name: Check if tag exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        id: check_std_tag
+        id: check_batteries_tag
         run: |
           git config user.name "leanprover-community-mathlib4-bot"
           git config user.email "[email protected]"
 
           if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
             BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
           else
-            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Std. Falling back to 'nightly-testing'."
+            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi
 
@@ -268,7 +268,7 @@ jobs:
           else
             echo "Branch already exists, pushing an empty commit."
             git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
-            # The Std `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
+            # The Batteries `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
             # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
             git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
             git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
@@ -321,7 +321,7 @@ jobs:
             git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
             echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
             git add lean-toolchain
-            sed -i "s/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \".\+\"/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
+            sed -i "s/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \".\+\"/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
             git add lakefile.lean
             git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           else

RELEASES.md

@@ -11,7 +11,18 @@ of each version.
 v4.9.0 (development in progress)
 ---------
 
-v4.8.0 
+* Functions defined by well-founded recursion are now marked as
+  `@[irreducible]`, which should prevent expensive and often unfruitful
+  unfolding of such definitions.
+
+  Existing proofs that hold by definitional equality (e.g. `rfl`) can be
+  rewritten to explictly unfold the function definition (using `simp`,
+  `unfold`, `rw`), or the recursive function can be temporariliy made
+  semireducible (using `unseal f in` before the command) or the function
+  definition itself can be marked as `@[semireducible]` to get the previous
+  behavor.
+
+v4.8.0
 ---------
 
 * **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**

doc/BoolExpr.lean

@@ -1,4 +1,4 @@
-open Std
+open Batteries
 open Lean
 
 inductive BoolExpr where

doc/dev/release_checklist.md

@@ -50,13 +50,13 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR
       - Create and push the tag
       - Merge the tag into `stable`
-    - [Std](https://github.com/leanprover-community/std4)
+    - [Batteries](https://github.com/leanprover-community/batteries)
       - No dependencies
       - Toolchain bump PR
       - Create and push the tag
       - Merge the tag into `stable`
     - [ProofWidgets4](https://github.com/leanprover-community/ProofWidgets4)
-      - Dependencies: `Std`
+      - Dependencies: `Batteries`
       - Note on versions and branches:
         - `ProofWidgets` uses a sequential version tagging scheme, e.g. `v0.0.29`,
           which does not refer to the toolchain being used.
@@ -65,7 +65,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Toolchain bump PR
       - Create and push the tag, following the version convention of the repository
     - [Aesop](https://github.com/leanprover-community/aesop)
-      - Dependencies: `Std`
+      - Dependencies: `Batteries`
       - Toolchain bump PR including updated Lake manifest
       - Create and push the tag
       - Merge the tag into `stable`
@@ -79,7 +79,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - Create and push the tag
       - There is no `stable` branch; skip this step
     - [Mathlib](https://github.com/leanprover-community/mathlib4)
-      - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Std`, `doc-gen4`, `import-graph`
+      - Dependencies: `Aesop`, `ProofWidgets4`, `lean4checker`, `Batteries`, `doc-gen4`, `import-graph`
       - Toolchain bump PR notes:
         - In addition to updating the `lean-toolchain` and `lakefile.lean`,
           in `.github/workflows/build.yml.in` in the `lean4checker` section update the line
@@ -123,8 +123,8 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
 
 - Decide which nightly release you want to turn into a release candidate.
   We will use `nightly-2024-02-29` in this example.
-- It is essential that Std and Mathlib already have reviewed branches compatible with this nightly.
-  - Check that both Std and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
+- It is essential that Batteries and Mathlib already have reviewed branches compatible with this nightly.
+  - Check that both Batteries and Mathlib's `bump/v4.7.0` branch contain `nightly-2024-02-29`
     in their `lean-toolchain`.
   - The steps required to reach that state are beyond the scope of this checklist, but see below!
 - Create the release branch from this nightly tag:
@@ -182,7 +182,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
   - We do this for the same list of repositories as for stable releases, see above.
     As above, there are dependencies between these, and so the process above is iterative.
     It greatly helps if you can merge the `bump/v4.7.0` PRs yourself!
-  - For Std/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
+  - For Batteries/Aesop/Mathlib, which maintain a `nightly-testing` branch, make sure there is a tag
     `nightly-testing-2024-02-29` with date corresponding to the nightly used for the release
     (create it if not), and then on the `nightly-testing` branch `git reset --hard master`, and force push.
 - Make an announcement!
@@ -204,7 +204,7 @@ In particular, updating the downstream repositories is significantly more work
 # Preparing `bump/v4.7.0` branches
 
 While not part of the release process per se,
-this is a brief summary of the work that goes into updating Std/Aesop/Mathlib to new versions.
+this is a brief summary of the work that goes into updating Batteries/Aesop/Mathlib to new versions.
 
 Please read https://leanprover-community.github.io/contribute/tags_and_branches.html
 

doc/monads/states.lean

@@ -15,7 +15,7 @@ data type containing several important pieces of information. First and foremost
 current player, and it has a random generator.
 -/
 
-open Std (HashMap)
+open Batteries (HashMap)
 abbrev TileIndex := Nat × Nat -- a 2D index
 
 inductive TileState where

src/Init/Core.lean

@@ -1114,9 +1114,6 @@ theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by
   cases a
   exact rfl
 
-instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : Inhabited {x // p x} where
-  default := ⟨a, h⟩
-
 instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
   fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
     if h : a = b then isTrue (by subst h; exact rfl)

src/Init/Data/Array/Basic.lean

@@ -733,17 +733,15 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
   if h : i.val + 1 < a.size then
     let a' := a.swap ⟨i.val + 1, h⟩ i
     let i' : Fin a'.size := ⟨i.val + 1, by simp [a', h]⟩
-    have : a'.size - i' < a.size - i := by
-      simp [a', Nat.sub_succ_lt_self _ _ i.isLt]
     a'.feraseIdx i'
   else
     a.pop
 termination_by a.size - i.val
-decreasing_by simp_wf; decreasing_trivial_pre_omega
+decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
 
 theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
   induction a, i using Array.feraseIdx.induct with
-  | @case1 a i h a' _ _ ih =>
+  | @case1 a i h a' _ ih =>
     unfold feraseIdx
     simp [h, a', ih]
   | case2 a i h =>

src/Init/Data/Array/Lemmas.lean

@@ -943,7 +943,7 @@ theorem anyM_loop_iff_exists (p : α → Bool) (as : Array α) (start stop) (h :
     omega
 termination_by stop - start
 
--- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Std.Data.Array.Init.Monadic`
+-- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
 theorem any_iff_exists (p : α → Bool) (as : Array α) (start stop) :
     any as p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by
   dsimp [any, anyM, Id.run]

src/Init/Data/Array/Subarray.lean

@@ -22,7 +22,7 @@ abbrev Subarray.as (s : Subarray α) : Array α := s.array
 theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
 
 @[deprecated Subarray.stop_le_array_size]
-theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.as.size := s.stop_le_array_size
+theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size
 
 namespace Subarray
 

src/Init/Data/BitVec/Bitblast.lean

@@ -184,4 +184,126 @@ theorem bit_neg_eq_neg (x : BitVec w) : -x = (adc (((iunfoldr (fun (i : Fin w) c
     simp [← sub_toAdd, BitVec.sub_add_cancel]
   · simp [bit_not_testBit x _]
 
+/-!
+### Multiplication
+We implement [Booth's multiplication circuit](https://en.wikipedia.org/wiki/Booth%27s_multiplication_algorithm)
+on bitvectors, and show that this circuit is equal to our straightforward `BitVec.mul` implementation.
+-/
+
+def mulAdd (a x y : BitVec w) : BitVec w :=
+  Prod.snd <| iunfoldr (s:=a) fun (i : Fin w) a =>
+    let a := if y.getLsb i = true then a + x else a
+    (a >>> 1, a.getLsb 0)
+
+def mulAddAccumulator (a x y : BitVec w) (i : Nat) : BitVec w :=
+  (a + x * (y.truncate i |>.zeroExtend _)) >>> i
+
+@[simp] theorem truncate_zero : truncate 0 x = 0#0 := of_length_zero
+
+@[simp] theorem mul_zero (x : BitVec w) : x * 0#w = 0#w := rfl
+@[simp] theorem shiftRight_zero (x : BitVec w) : x >>> 0 = x := rfl
+@[simp] theorem shiftLeft_zero (x : BitVec w) : x <<< 0 = x := by apply eq_of_toNat_eq; simp
+
+theorem mulAddAccumulator_zero (a x y : BitVec w) : mulAddAccumulator a x y 0 = a := by
+  simp [mulAddAccumulator]
+
+theorem Nat.shiftRight_add' (m n k : Nat) :
+    m >>> n + k = (m + (k <<< n)) >>> n := by
+  sorry
+
+theorem shiftRight_add' (x y : BitVec w) (n : Nat) :
+    x >>> n + y = (x + (y <<< n)) >>> n := by
+  sorry
+
+#check BitVec.shiftRight_shiftRight
+
+theorem zeroExtend_truncate_eq_and (x : BitVec w) (i : Nat) :
+    zeroExtend w (x.truncate i) = x &&& ((-1 : BitVec _) >>> (w-i)) := by
+  sorry
+
+theorem add_shiftRight (x y : BitVec w) (n : Nat) : (x + y) >>> n = (x >>> n) + (y >>> n) := by
+  sorry
+
+@[simp] theorem zero_shiftRight (w n : Nat) : 0#w >>> n = 0#w := by
+  sorry
+
+theorem mod_two_pow_shiftRight (x m n : Nat) : (x % 2^m) >>> n = (x >>> n) % (2^(m+n)) := by
+  induction n
+  case zero => rfl
+  case succ n ih =>
+    simp [shiftRight_succ]
+    sorry
+
+theorem shiftLeft_shiftRight_eq_zeroExtend_truncate (x : BitVec w) (i : Nat) :
+    x <<< i >>> i = zeroExtend w (truncate (w-i) x) := by
+  apply eq_of_toNat_eq
+  simp only [toNat_ushiftRight, toNat_shiftLeft, toNat_truncate]
+  induction i
+  case a.zero => simp
+  case a.succ i ih =>
+    rw [mod_two_pow_shiftRight]
+    sorry
+
+theorem mulAddAccumulator_succ (a x y : BitVec w) :
+    mulAddAccumulator a x y (i+1)
+    = (mulAddAccumulator a x y i >>> 1)
+      + bif y.getLsb (i+1) then (x.truncate (i+1) |>.zeroExtend _) else 0#w := by
+  -- ext j
+  simp only [mulAddAccumulator, natCast_eq_ofNat, BitVec.shiftRight_shiftRight]
+  have :
+      x * zeroExtend w (truncate (i + 1) y)
+      = x * zeroExtend w (truncate i y) + (bif y.getLsb (i+1) then x <<< (i+1) else 0) := by
+    simp [← shiftLeft_shiftRight_eq_zeroExtend_truncate]
+  rw [this, ← BitVec.add_assoc, add_shiftRight]
+  congr
+  cases y.getLsb (i+1)
+  · simp
+  · simp; sorry
+
+
+
+
+@[simp]
+theorem zeroExtend_zero_width (x : BitVec 0) : zeroExtend w x = 0#w := by
+  sorry
+
+-- @[simp] theorem shiftRight_zero (x : BitVec w) : x >>> 0 = x := rfl
+-- @[simp] theorem mul_zero (x : BitVec w) : x * 0#w = 0#w := rfl
+
+theorem extractLsb'_succ_eq_concat (x : BitVec w) (s n : Nat) :
+    x.extractLsb' s (n+1) = cons (x.getLsb (s+n)) (x.extractLsb' s n) := by
+  sorry
+
+theorem mulAdd_spec (a x y : BitVec w):
+    mulAdd a x y = a + x * y := by
+  simp only [mulAdd]
+  rw [iunfoldr_replace (state := mulAddAccumulator a x y)]
+  · simp [mulAddAccumulator, Nat.mod_one]
+  · intro i
+    simp only [mulAddAccumulator, Prod.mk.injEq, natCast_eq_ofNat]
+    cases y.getLsb i <;> simp
+    · sorry
+    · sorry
+
+theorem getLsb_mul (x y : BitVec w) (i : Fin w) :
+    (x * y).getLsb i = Bool.xor (x.getLsb i && y.getLsb i) ((mulAddAccumulator 0 x y i).getLsb 0) := by
+  sorry
+
+theorem zeroExtend'_mul_zeroExtend' (x y : BitVec w) (h : w ≤ v) :
+    x.zeroExtend' h * y.zeroExtend' h = (x * y).zeroExtend' h := by
+  sorry
+
+@[simp] theorem zeroExtend'_rfl (x : BitVec w) (h : w ≤ w := by rfl) : x.zeroExtend' h = x := rfl
+
+@[simp] theorem truncate_zeroExtend' (x : BitVec w) (h : w ≤ v) : truncate w (x.zeroExtend' h) = x := by
+  simp [truncate, zeroExtend]
+  intro h'
+  have h_eq : w = v := Nat.le_antisymm h h'
+  subst h_eq
+  simp [h']
+
+theorem mul_eq_mulAdd (x y : BitVec w) :
+    x * y = (mulAdd 0 x y).truncate w := by
+  simp [mulAdd_spec]
+
 end BitVec