Documentation

Complexity.Computability.Circuit.Boolean.Iteration.Remainder

Remainders modulo an available word #

The remainder of an m-bit number modulo a nonzero w-bit word d is computed by long division, from the most significant bit: shift the current remainder, append the next bit, and subtract d once if the result is at least d (streamRemainder). If 2 * d fits in w bits, the shifted remainder never overflows, and the result is exact (toNat_streamRemainder). Each bit costs one subtraction, one comparison and one selection, 22 * w + 3 gates, so the cost is linear in the number of bits for a fixed modulus width (synthesis_streamRemainder). In particular an m-bit number modulo a nonzero k-bit input modulus has a circuit of size 1 + m * (22 * (k + 1) + 3) (bounded_modulus_remainder).

Reducing both arguments this way gives a difference modulo d in O(w ^ 2) gates (subMod, synthesis_subMod).

All gates of the native De Morgan basis, including constants, are charged; wiring and fanout are free.

Main definitions #

Main results #

References #

source
theorem Cslib.Circuits.Boolean.Iteration.word_succ {m : ℕ} (bits : BitString (m + 1)) :
word bits = (word fun (i : Fin m) => bits i.succ).concat (bits 0)

A word with one more bit, read from the least significant end.

Streaming remainders #

source
def Cslib.Circuits.Boolean.Iteration.remainderStep {w : ℕ} (d r : BitVec w) (b : Bool) :
BitVec w

One step of long division by d: append bit b to the remainder r and subtract d once if the result is at least d.

Instances For
    source
    def Cslib.Circuits.Boolean.Iteration.streamRemainder {w : ℕ} (d : BitVec w) {m : ℕ} :
    BitString m → BitVec w

    The remainder modulo d of the number with the given bits, least significant first, by long division from the most significant bit.

    Instances For
      source
      theorem Cslib.Circuits.Boolean.Iteration.toNat_remainderStep {w : ℕ} (d r : BitVec w) (b : Bool) (hd : 0 < d.toNat) (hw : 2 * d.toNat ≤ 2 ^ w) (hr : r.toNat < d.toNat) :
      (remainderStep d r b).toNat = (2 * r.toNat + b.toNat) % d.toNat
      source
      theorem Cslib.Circuits.Boolean.Iteration.toNat_streamRemainder {m w : ℕ} (d : BitVec w) (bits : BitString m) (hd : 0 < d.toNat) (hw : 2 * d.toNat ≤ 2 ^ w) :
      (streamRemainder d bits).toNat = (word bits).toNat % d.toNat

      Streaming remainders. If 0 < d and 2 * d fits in the word width, the streamed remainder is the value of the bits modulo d.

      source
      theorem Cslib.Circuits.Boolean.Iteration.synthesis_remainderStep {a w : ℕ} (s : Set (BooleanFunction a)) (d r : BitString a → BitVec w) (b : BooleanFunction a) (hd : ∀ (i : Fin w), (fun (x : BitString a) => (d x).getLsbD ↑i) ∈ s) (hr : ∀ (i : Fin w), (fun (x : BitString a) => (r x).getLsbD ↑i) ∈ s) (hb : b ∈ s) :
      Synthesis interpretation s (wordWires fun (x : BitString a) => remainderStep (d x) (r x) (b x)) (22 * w + 3)

      One step of long division: a subtraction, a comparison and a selection.

      source
      theorem Cslib.Circuits.Boolean.Iteration.synthesis_streamRemainder {a m w : ℕ} (s : Set (BooleanFunction a)) (d : BitString a → BitVec w) (bits : BitString a → BitString m) (hd : ∀ (i : Fin w), (fun (x : BitString a) => (d x).getLsbD ↑i) ∈ s) (hb : ∀ (j : Fin m), (fun (x : BitString a) => bits x j) ∈ s) (hz : (fun (x : BitString a) => false) ∈ s) :
      Synthesis interpretation s (wordWires fun (x : BitString a) => streamRemainder (d x) (bits x)) (m * (22 * w + 3))

      Streaming an available m-bit number through long division by an available word costs 22 * w + 3 gates per bit.

      source
      theorem Cslib.Circuits.Boolean.Iteration.bounded_modulus_remainder (m k : ℕ) :
      ∃ (out : Circuit signature (m + k) k), (∀ (x : Fin (m + k) → Bool), 0 < (word fun (i : Fin k) => x (Fin.natAdd m i)).toNat → (word (out.eval interpretation x)).toNat = (word fun (i : Fin m) => x (Fin.castAdd k i)).toNat % (word fun (i : Fin k) => x (Fin.natAdd m i)).toNat) ∧ out.size ≤ 1 + m * (22 * (k + 1) + 3)

      Bounded-modulus remainders. Some circuit of size at most 1 + m * (22 * (k + 1) + 3) reads an m-bit number and then a k-bit modulus, both least significant bit first, and returns the number modulo the modulus whenever the modulus is nonzero. The circuit is total; nothing is claimed about its output for the zero modulus.

      Modular differences #

      source
      def Cslib.Circuits.Boolean.Iteration.subMod {w : ℕ} (a b d : BitVec w) :
      BitVec w

      a - b modulo d, from the remainders of a and b: their difference, plus d if it would be negative.

      Instances For
        source
        theorem Cslib.Circuits.Boolean.Iteration.add_sub_mod_mod_eq_ite (a b d : ℕ) (hd : 0 < d) :
        (a + d - b % d) % d = if a % d < b % d then a % d + d - b % d else a % d - b % d
        source
        theorem Cslib.Circuits.Boolean.Iteration.add_sub_mod_mod_eq_of_modEq {a b c d : ℕ} (hd : 0 < d) (hc : c < d) (he : c + b ≡ a [MOD d]) :
        (a + d - b % d) % d = c

        A modular difference is determined by the congruence it satisfies.

        source
        theorem Cslib.Circuits.Boolean.Iteration.toNat_subMod {w : ℕ} (a b d : BitVec w) (hd : 0 < d.toNat) (hw : 2 * d.toNat ≤ 2 ^ w) :
        (subMod a b d).toNat = (a.toNat + d.toNat - b.toNat % d.toNat) % d.toNat

        Modular differences. If 0 < d and 2 * d fits in the word width, subMod a b d is a - b modulo d, in the form (a + d - b % d) % d.

        source
        theorem Cslib.Circuits.Boolean.Iteration.synthesis_subMod {n w : ℕ} (s : Set (BooleanFunction n)) (a b d : BitString n → BitVec w) (ha : ∀ (i : Fin w), (fun (x : BitString n) => (a x).getLsbD ↑i) ∈ s) (hb : ∀ (i : Fin w), (fun (x : BitString n) => (b x).getLsbD ↑i) ∈ s) (hd : ∀ (i : Fin w), (fun (x : BitString n) => (d x).getLsbD ↑i) ∈ s) (hz : (fun (x : BitString n) => false) ∈ s) :
        Synthesis interpretation s (wordWires fun (x : BitString n) => subMod (a x) (b x) (d x)) (50 * (w + 1) ^ 2)

        A modular difference of available words costs two streaming remainders and a constant number of word operations: at most 50 * (w + 1) ^ 2 gates.