Documentation

Complexity.Algorithms.WordRAM.ExactTriangle.Chunks

Native query-chunk descriptors #

For one computed query class, the program writes consecutive triples (residue, pair pointer, pair count). It computes the last chunk's shorter length and advances over the actual two-word coordinate representation. The input query list is preserved.

This adapts the chunk loop in the pinned Theorem 17 chunk builder.

Main definitions #

Main results #

source
@[reducible, inline]
abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Chunks.queries :
Fin 14

Query pair array base.

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

    Descriptor output base.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Chunks.total :
      Fin 14

      Actual number of query pairs.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Chunks.capacity :
        Fin 14

        Positive maximum pairs per chunk.

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

          Class residue.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Chunks.pos :
            Fin 14

            Consumed pair count.

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

              Number of written chunks.

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

                Constant one.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Chunks.three :
                  Fin 14

                  Number of words per descriptor.

                  Instances For
                    source
                    @[reducible, inline]
                    abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Chunks.length :
                    Fin 14

                    Current chunk length.

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

                      Output address.

                      Instances For
                        source
                        @[reducible, inline]
                        abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Chunks.ptr :
                        Fin 14

                        Current pair pointer.

                        Instances For
                          source
                          def Cslib.Algorithms.WordRAM.ExactTriangle.Chunks.body :
                          WordRAM.Code WordRAM.Basis.standard 14

                          Compute a nonempty chunk, write its descriptor and advance both counters.

                          Instances For
                            source
                            def Cslib.Algorithms.WordRAM.ExactTriangle.Chunks.program :
                            WordRAM.Code WordRAM.Basis.standard 14

                            Initialize all loop state with charged instructions.

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

                              Fixed code and no physical-width reads.

                              source
                              theorem Cslib.Algorithms.WordRAM.ExactTriangle.Chunks.exec {w : ℕ} (x : WordRAM.Data 14) (hcap : 0 < x.regs capacity) (hfit : WordRAM.Fits w (x.regs dst + 3 * x.regs total + 3)) (hquery : WordRAM.Fits w (x.regs queries + 2 * x.regs total)) :
                              ∃ (y : WordRAM.Data 14), WordRAM.ExecWithin w program x y (17 * x.regs total + 7) ∧ y.regs count = x.regs total ⌈/⌉ x.regs capacity ∧ (∀ (i : Fin 14), ↑i < 5 → y.regs i = x.regs i) ∧ (∀ k < y.regs count, y.mem (x.regs dst + 3 * k) = x.regs residue ∧ y.mem (x.regs dst + 3 * k + 1) = x.regs queries + 2 * (k * x.regs capacity) ∧ y.mem (x.regs dst + 3 * k + 2) = min (x.regs capacity) (x.regs total - k * x.regs capacity)) ∧ ∀ (a : ℕ), ¬(x.regs dst ≤ a ∧ a < x.regs dst + 3 * y.regs count) → y.mem a = x.mem a

                              Write the exact nonempty chunks of one class. Descriptor k names the query slice beginning at pair k * capacity, with its final length truncated to the class size. All other memory is preserved, so placing the query array outside the descriptor block preserves its coordinates. The final halt is excluded from the 17 total + 7 bound.