Documentation

Complexity.Algorithms.WordRAM.PrimeTable

Native prime tables #

This fixed program tests every candidate through the supplied bound, writes its primality bit, and counts the primes. Trial division, table addresses, writes and loops are charged. There is no primality oracle or assumed sieve.

Main definitions #

Main results #

source
def Cslib.Algorithms.WordRAM.PrimeTable.trialRegisters (i : Fin 6) :
Fin 15

Registers of the trial-division subroutine.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Algorithms.WordRAM.PrimeTable.arg :
    Fin 15

    Current trial-division candidate.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Algorithms.WordRAM.PrimeTable.flag :
      Fin 15

      Current candidate's primality bit.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.Algorithms.WordRAM.PrimeTable.limit :
        Fin 15

        Largest candidate.

        Instances For
          source
          @[reducible, inline]
          abbrev Cslib.Algorithms.WordRAM.PrimeTable.base :
          Fin 15

          Output bitmap base.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.Algorithms.WordRAM.PrimeTable.cursor :
            Fin 15

            First candidate not yet written.

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

              Address scratch.

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

                Number of primes written.

                Instances For
                  source
                  @[reducible, inline]
                  abbrev Cslib.Algorithms.WordRAM.PrimeTable.stop :
                  Fin 15

                  One past the largest candidate.

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

                    Constant one.

                    Instances For
                      source
                      @[reducible, inline]
                      abbrev Cslib.Algorithms.WordRAM.PrimeTable.zero :
                      Fin 15

                      Constant zero.

                      Instances For
                        source
                        @[reducible, inline]
                        abbrev Cslib.Algorithms.WordRAM.PrimeTable.two :
                        Fin 15

                        Constant two.

                        Instances For
                          source
                          def Cslib.Algorithms.WordRAM.PrimeTable.test :
                          WordRAM.Code WordRAM.Basis.standard 15

                          Handle zero and one directly; test all larger candidates by charged native trial division.

                          Instances For
                            source
                            def Cslib.Algorithms.WordRAM.PrimeTable.body :
                            WordRAM.Code WordRAM.Basis.standard 15

                            Test, write the bit, update the count, and advance the candidate.

                            Instances For
                              source
                              def Cslib.Algorithms.WordRAM.PrimeTable.program :
                              WordRAM.Code WordRAM.Basis.standard 15

                              A finite native prime-table program with its bound and base supplied in registers.

                              Instances For
                                source
                                def Cslib.Algorithms.WordRAM.PrimeTable.memory (mem : ℕ → ℕ) (base k : ℕ) :
                                ℕ → ℕ

                                The first k primality bits, preserving all other memory cells.

                                Instances For
                                  source
                                  theorem Cslib.Algorithms.WordRAM.PrimeTable.exec {w : ℕ} (x : WordRAM.Data 15) (hfit : WordRAM.Fits w (x.regs limit + 3)) (haddr : WordRAM.Fits w (x.regs base + (x.regs limit + 1))) :
                                  ∃ (y : WordRAM.Data 15), WordRAM.ExecWithin w program x y ((x.regs limit + 1) * (7 * x.regs limit + 15) + 8) ∧ y.mem = memory x.mem (x.regs base) (x.regs limit + 1) ∧ y.regs count = (x.regs limit).primesLE.card ∧ y.regs limit = x.regs limit ∧ y.regs base = x.regs base

                                  Write every primality bit through m, count exactly Nat.primesLE m, and preserve all cells outside the bitmap. Trial division gives the explicit quadratic bound (m+1)(7m+15)+8; the final halt is excluded.