Documentation

Complexity.Algorithms.WordRAM.Deduplicate.Count

Native counting of one adjacent run #

The counter tests the array bound before every read and stops at the first different word. No sorting or counting oracle is used. The mathematical end index is a proof parameter and does not occur in the code or a register.

Main definitions #

Main results #

source
@[reducible, inline]
abbrev Cslib.Algorithms.WordRAM.Deduplicate.len :
Fin 16

Input length.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Algorithms.WordRAM.Deduplicate.src :
    Fin 16

    Sorted input array.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Algorithms.WordRAM.Deduplicate.keys :
      Fin 16

      Unique-key output array.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.Algorithms.WordRAM.Deduplicate.counts :
        Fin 16

        Multiplicity output array.

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

          Input cursor.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.Algorithms.WordRAM.Deduplicate.out :
            Fin 16

            Number of completed output runs.

            Instances For
              source
              @[reducible, inline]
              abbrev Cslib.Algorithms.WordRAM.Deduplicate.key :
              Fin 16

              Current run key.

              Instances For
                source
                @[reducible, inline]
                abbrev Cslib.Algorithms.WordRAM.Deduplicate.count :
                Fin 16

                Current run multiplicity.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev Cslib.Algorithms.WordRAM.Deduplicate.value :
                  Fin 16

                  Loaded input word.

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

                    Address temporary.

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

                      Constant one.

                      Instances For
                        source
                        @[reducible, inline]
                        abbrev Cslib.Algorithms.WordRAM.Deduplicate.active :
                        Fin 16

                        Run-counting loop flag.

                        Instances For
                          source
                          def Cslib.Algorithms.WordRAM.Deduplicate.Count.body :
                          WordRAM.Code WordRAM.Basis.standard 16

                          Read the next word only if the cursor is in bounds; count it or end the run.

                          Instances For
                            source
                            def Cslib.Algorithms.WordRAM.Deduplicate.Count.code :
                            WordRAM.Code WordRAM.Basis.standard 16

                            Count from the current cursor, starting with zero count and flag one.

                            Instances For
                              source
                              theorem Cslib.Algorithms.WordRAM.Deduplicate.Count.exec {w s n start stop k : ℕ} (x : WordRAM.Data 16) (hn : x.regs len = n) (hs : x.regs src = s) (hi : x.regs idx = start) (hk : x.regs key = k) (hc : x.regs count = 0) (ha : x.regs active = 1) (ho : x.regs one = 1) (hle : start ≤ stop) (hstop : stop ≤ n) (hmem : ∀ (j : ℕ), start ≤ j → j < stop → x.mem (s + j) = k) (hnext : stop < n → x.mem (s + stop) ≠ k) (hfit : WordRAM.Fits w (s + n)) :
                              ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin w code x y (8 * (stop - start) + 10) ∧ y.regs idx = stop ∧ y.regs count = stop - start ∧ y.mem = x.mem

                              Count a maximal adjacent run in 8c+10 instructions, including the terminating test. stop is a proof parameter: execution learns the boundary solely through charged comparisons and loads. The source memory is unchanged. Empty runs are also admitted by this kernel.