Documentation

Complexity.Algorithms.WordRAM.ExactTriangle.Classes

Native residue-class query lists #

The fixed program calls QueryScan.program for each residue, storing the computed class count and its row-major coordinate pairs. Each class receives a disjoint block of capacity 2n². The cost of scanning once per residue is included; no class table is supplied as input.

This adapts the class builder in the pinned Theorem 17 program.

Main definitions #

Main results #

source
@[reducible, inline]
abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Classes.src :
Fin 20

Source residue matrix.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Classes.dst :
    Fin 20

    Query-scanner output pointer.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Classes.size :
      Fin 20

      Matrix side.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Classes.residue :
        Fin 20

        Query-scanner selected residue.

        Instances For
          source
          @[reducible, inline]
          abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Classes.count :
          Fin 20

          Query-scanner emitted count.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Classes.counts :
            Fin 20

            Array of class counts.

            Instances For
              source
              @[reducible, inline]
              abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Classes.queries :
              Fin 20

              Array of disjoint query blocks.

              Instances For
                source
                @[reducible, inline]
                abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Classes.modulus :
                Fin 20

                Number of residues to enumerate.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Classes.cursor :
                  Fin 20

                  Current class.

                  Instances For
                    source
                    @[reducible, inline]
                    abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Classes.one :
                    Fin 20

                    Constant one.

                    Instances For
                      source
                      @[reducible, inline]
                      abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Classes.addr :
                      Fin 20

                      Count address.

                      Instances For
                        source
                        @[reducible, inline]
                        abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Classes.stride :
                        Fin 20

                        Capacity in words of a query block.

                        Instances For
                          source
                          def Cslib.Algorithms.WordRAM.ExactTriangle.Classes.scan :
                          WordRAM.Code WordRAM.Basis.standard 20

                          Reuse the certified scanner with a disjoint register bank for the outer loop.

                          Instances For
                            source
                            def Cslib.Algorithms.WordRAM.ExactTriangle.Classes.body :
                            WordRAM.Code WordRAM.Basis.standard 20

                            Compute the class's output pointer, scan, record its count, and advance.

                            Instances For
                              source
                              def Cslib.Algorithms.WordRAM.ExactTriangle.Classes.program :
                              WordRAM.Code WordRAM.Basis.standard 20

                              The modulus is runtime data; the program itself is independent of it.

                              Instances For
                                source
                                theorem Cslib.Algorithms.WordRAM.ExactTriangle.Classes.program_fixed :
                                program.size ≤ 64 ∧ ¬program.ReadsWidth

                                Fixed instruction graph, with no physical-width reads.

                                source
                                theorem Cslib.Algorithms.WordRAM.ExactTriangle.Classes.exec {w : ℕ} (x : WordRAM.Data 20) (R : ℕ → ℕ) (h1 : WordRAM.Fits w 1) (hinput : ∀ q < x.regs size * x.regs size, x.mem (x.regs src + q) = R q) (hsource : x.regs src + x.regs size * x.regs size ≤ x.regs counts) (hblocks : x.regs counts + x.regs modulus ≤ x.regs queries) (hcount : WordRAM.Fits w (x.regs counts + x.regs modulus)) (hquery : WordRAM.Fits w (x.regs queries + 2 * (x.regs size * x.regs size) * x.regs modulus)) (harea : WordRAM.Fits w (2 * (x.regs size * x.regs size))) :
                                ∃ (y : WordRAM.Data 20), WordRAM.ExecWithin w program x y (x.regs modulus * (14 * (x.regs size * x.regs size) + 14) + 6) ∧ y.regs cursor = x.regs modulus ∧ (∀ j < x.regs modulus, y.mem (x.regs counts + j) = Nat.count (fun (q : ℕ) => R q = j) (x.regs size * x.regs size)) ∧ (∀ j < x.regs modulus, ∀ q < x.regs size * x.regs size, R q = j → y.mem (x.regs queries + 2 * (x.regs size * x.regs size) * j + 2 * Nat.count (fun (k : ℕ) => R k = j) q) = q / x.regs size ∧ y.mem (x.regs queries + 2 * (x.regs size * x.regs size) * j + 2 * Nat.count (fun (k : ℕ) => R k = j) q + 1) = q % x.regs size) ∧ ∀ (a : ℕ), ¬(x.regs counts ≤ a ∧ a < x.regs counts + x.regs modulus) → ¬(x.regs queries ≤ a ∧ a < x.regs queries + 2 * (x.regs size * x.regs size) * x.regs modulus) → y.mem a = x.mem a

                                Enumerate every residue class into actual count and coordinate arrays. The source matrix, count array and query capacity blocks must occur in that order. The final halt is excluded.