Documentation

Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.CollisionTest

Native tests of the three Chan–He collision inequalities #

Each inequality multiplies a computed collision count by the number of candidate primes, then compares it with its supplied threshold. All multiplications, branches and flag updates are ordinary charged instructions. No predicate is executed by an oracle.

Main definitions #

Main results #

source
@[reducible, inline]
abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CollisionTest.card :
Fin 64

Number of candidate primes.

Instances For
    source
    def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CollisionTest.threshold (j : Fin 3) :
    Fin 64

    Threshold for one of the three sets.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CollisionTest.zero :
      Fin 64

      Constant zero.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CollisionTest.scaled :
        Fin 64

        Collision count times the number of candidate primes.

        Instances For
          source
          @[reducible, inline]
          abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CollisionTest.good :
          Fin 64

          Acceptance flag.

          Instances For
            source
            def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CollisionTest.compare (j : Fin 3) :
            WordRAM.Code WordRAM.Basis.standard 64

            One charged multiplication and comparison, retaining a previously false flag.

            Instances For
              source
              def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CollisionTest.program :
              WordRAM.Code WordRAM.Basis.standard 64

              Initialize a true flag and test all three supplied collision counts.

              Instances For
                source
                theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CollisionTest.exec {w : ℕ} (x : WordRAM.Data 64) (h1 : WordRAM.Fits w 1) (hz : x.regs zero = 0) (hfit : ∀ (j : Fin 3), WordRAM.Fits w (x.regs (CountCall.result j) * x.regs card)) :
                ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin w program x y 13 ∧ (y.regs good = if x.regs (CountCall.result 0) * x.regs card ≤ x.regs (threshold 0) ∧ x.regs (CountCall.result 1) * x.regs card ≤ x.regs (threshold 1) ∧ x.regs (CountCall.result 2) * x.regs card ≤ x.regs (threshold 2) then 1 else 0) ∧ y.mem = x.mem ∧ ∀ (i : Fin 64), i ≠ scaled → i ≠ good → y.regs i = x.regs i

                Test all three inequalities with a shared acceptance flag. The only written registers are scaled and good; memory and every other caller register are unchanged.