Documentation

Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.Residues

Native Euclidean residue arrays #

The input holds signed encodings. The output holds ordinary unsigned residue keys, ready for histogram construction. In particular a nonnegative encoded integer is explicitly decoded by division by two before it is used as a histogram index.

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Residues.src :
Fin 16

Encoded integer input base.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Residues.dst :
    Fin 16

    Unsigned residue output base.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Residues.len :
      Fin 16

      Input length.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Residues.modulus :
        Fin 16

        Encoded modulus.

        Instances For
          source
          @[reducible, inline]
          abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Residues.idx :
          Fin 16

          Loop counter.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Residues.addr :
            Fin 16

            Address scratch.

            Instances For
              source
              @[reducible, inline]
              abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Residues.one :
              Fin 16

              Constant one.

              Instances For
                source
                def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Residues.body :
                WordRAM.Code WordRAM.Basis.standard 16

                The signed remainder block followed by explicit unsigned decoding and a store.

                Instances For
                  source
                  def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Residues.program :
                  WordRAM.Code WordRAM.Basis.standard 16

                  All parameters are supplied at runtime; registers and code are independent of length and width.

                  Instances For
                    source
                    def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Residues.memory (mem : ℕ → ℕ) (values : ℕ → ℤ) (M dst k : ℕ) :
                    ℕ → ℕ

                    Memory after writing a prefix of unsigned residue keys.

                    Instances For
                      source
                      @[simp]
                      theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Residues.memory_zero (mem : ℕ → ℕ) (values : ℕ → ℤ) (M dst : ℕ) :
                      memory mem values M dst 0 = mem
                      source
                      theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Residues.exec {w M : ℕ} (x : WordRAM.Data 16) (values : ℕ → ℤ) (hM : 0 < M) (hmod : GenericRAM.Signed.Fits w ↑M) (hmodreg : x.regs modulus = WordRAM.Signed.encode ↑M) (hfit : ∀ i < x.regs len, GenericRAM.Signed.Fits w (values i)) (hs : WordRAM.Fits (w + 2) (x.regs src + x.regs len)) (hd : WordRAM.Fits (w + 2) (x.regs dst + x.regs len)) (hdisj : x.regs src + x.regs len ≤ x.regs dst) (hinput : ∀ i < x.regs len, x.mem (x.regs src + i) = WordRAM.Signed.encode (values i)) :
                      ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin (w + 2) program x y (23 * x.regs len + 4) ∧ y.mem = memory x.mem values M (x.regs dst) (x.regs len) ∧ ∀ (i : Fin 16), 9 ≤ ↑i ∧ ↑i ≤ 12 → y.regs i = x.regs i

                      Convert n encoded signed integers to unsigned Euclidean residue keys in at most 23n + 4 native instructions. The modulus is positive and encoded in its parameter register; addresses are ordinary unsigned words. The final halt is excluded.