chore: write divmodstate explanation

Author: bollu

src/Init/Data/BitVec/Basic.lean

@@ -611,9 +611,8 @@ result of appending a single bit to the front in the naive implementation).
 def concat {n} (msbs : BitVec n) (lsb : Bool) : BitVec (n+1) := msbs ++ (ofBool lsb)
 
 /--
-Left shift `x` by `1` and then bitwise-or with `b`.
-This makes the least significant bit as `b`, and other bits are shifted left.
-This contrasts to `concatBit`, which actually extends the bitvector with a new bit.
+`x.shiftConcat b` shifts all bits of `x` to the left by `1` and sets the least significant bit to `b`.
+It is a non dependent version of `concat` that does not change the total bitwidth.
 -/
 def shiftConcat (x : BitVec n) (b : Bool) : BitVec n :=
   x <<< 1 ||| (ofBool b).zeroExtend n

src/Init/Data/BitVec/Bitblast.lean

@@ -431,32 +431,34 @@ theorem shiftLeft_eq_shiftLeftRec (x : BitVec w₁) (y : BitVec w₂) :
 
 /-! # udiv/urem recurrence for bitblasting
 
-Let us study an instructive counterexample to the claim that
-  `n = d * q + r` for (`0 ≤ r < d`) uniquely determining q and r *over bitvectors*.
+In order to prove the correctness of the division algorithm on the integers,
+one shows that `n.div d = q` and `n.mod d = r` iff `n = d * q + r` and `0 ≤ r < d`.
+Mnemonic: `n` is the numerator, `d` is the denominator, `q` is the quotient, and `r` the remainder.
+
+This uniqueness property is not true for bitvectors.
+Let us study an instructive counterexample:
 
 - Let `bitwidth = 3`
 - Let `n = 0, d = 3`
-- If we choose `q = 2, r = 2`, then d * q + r = 6 + 2 = 8 ≃ 0 (mod 8) so satisfies.
-- But see that `q = 0, r = 0` also satisfies, as 0 * 3 + 0 = 0.
-- So for (`n = 0, d = 3`), both:
-    `q = 2, r = 2` as well as
-    `q = 0, r = 0` are solutions!
+- If we choose `q = 2, r = 2`, then `d * q + r = 6 + 2 = 8 ≃ 0 (mod 8)` and (`r < d`).
+- But see that `q = 0, r = 0` also satisfies the constraints, as `0 * 3 + 0 = 0`.
+- So for (`n = 0, d = 3`), both (a) `q = 2, r = 2` as well as (b) `q = 0, r = 0` are solutions!
 
-It's easy to cook up such examples, by chosing `(q, r)` for a fixed `(d, n)`
-such that `(d * q + r)` overflows.
+Such examples can be created by choosing `(q, r)` for a fixed `(d, n)`
+such that `(d * q + r)` overflows and wraps around to equal `n`.
 
 This tells us that the division algorithm must have more restrictions that just the ones
 we have for natural numbers. These restrictions are captured in `DivModState.Lawful`,
 which captures the relationship necessary between `n, d, q, r`. The key idea is to state
-the relationship in terms of the `{n, d, q, r}.toNat` values, and then prove that the relationship
-holds for the bitvector values.
+the relationship in terms of the `{n, d, q, r}.toNat` values, which implies that the
+relationship also holds at the bitvector level.
 
 References:
 - Fast 32-bit Division on the DSP56800E: Minimized nonrestoring division algorithm by David Baca
 - Bitwuzla sources for bitblasting.h
 -/
 
-private theorem Nat.div_add_eq_left_of_lt {x y z : Nat} (hx : z ∣ x) (hy : y < z) (hz : 0 < z):
+private theorem Nat.div_add_eq_left_of_lt {x y z : Nat} (hx : z ∣ x) (hy : y < z) (hz : 0 < z) :
     (x + y) / z = x / z := by
   refine Nat.div_eq_of_lt_le ?lo ?hi
   · apply Nat.le_trans
@@ -519,9 +521,6 @@ This is a proof engineering choice: An alternative world could have
 
 Instead, we choose to declare all involved bitvectors as length `w`, and then prove that
 the values of `r` and `n` are within the bounds of `wr` and `wn` respectively.
-
-Note that `DivModState` manipulates thw widths of the remainder and the dividend,
-
 -/
 structure DivModState.Lawful (w wr wn : Nat) (n d : BitVec w)
     (qr : DivModState w) : Prop where
@@ -554,7 +553,7 @@ def DivModState.init (w : Nat) : DivModState w := {
   r := 0#w
 }
 
-/-- Make an initial state of the DivModState, for a given choice of `n, d, q, r`. -/
+/-- The initial state. -/
 def DivModState.Lawful.init (w : Nat) (n d : BitVec w) (hd : 0#w < d) :
     DivModState.Lawful w 0 w n d (DivModState.init w) := {
   hwrn := by omega,
@@ -593,6 +592,12 @@ theorem DivModState.umod_eq_of_lawful_zero {qr : DivModState w}
 
 /-! ### LawfulShiftSubtract -/
 
+/-!
+A `LawfulShiftSubtract` is a `Lawful` DivModState that is also a legal input to the shift subtractor.
+So in particular, we must have at least one dividend bit left over `(0 < wn)`
+to perform a round of shift subtraction.
+-/
+
 /--
 The input to the shift subtractor is a legal input to `divrem`, and we also need to have an
 input bit to perform shift subtraction on, and thus we need `0 < wn`.