Documentation

Complexity.Algorithms.WordRAM.ThreeSum.ChanHe.TraversalTime

Charged bounds for the native Chan–He worklist #

The per-node estimate includes both complete modulus searches and the complete packing program. It is cubic in the candidate bound, rather than quadratic in the input length. The root estimate also charges skipped calls, stack transfers, branches and loop control.

Main definitions #

Main results #

These estimates are original; their starting costs are the proved native execution bounds.

source
def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.visitTime (n m N : ℕ) :
ℕ

Both searches, the actual node program, argument delivery and the output-table store.

Instances For
    source
    def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.rootTime (f n m N : ℕ) :
    ℕ

    Root setup and every possible transition, including empty and zero-fuel entries.

    Instances For
      source
      def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.allocationSize (n m N : ℕ) :
      ℕ

      Three heavy count cells, three heavy buffers, four packed blocks, scratch and histogram.

      Instances For
        source
        theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.visit_cost_le (x : WordRAM.Data 128) (n m N M : ℕ) (hlen : ∀ (j : Fin 3), x.regs (arrayLength j) ≤ n) (hm : x.regs limit ≤ m) (hN : x.regs groups ≤ N) (hM : M ≤ m ^ 2) :
        Modulus.cost (WordRAM.Data.comap kernel (modulusState x)) + 66 * (recordLayout x M).total + 15 * M + 12 * x.regs groups + 277 ≤ visitTime n m N

        The exact charged cost from the complete native visit is uniformly bounded.

        source
        theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.allocation_le (x : WordRAM.Data 128) (n m N M : ℕ) (hlen : ∀ (j : Fin 3), x.regs (arrayLength j) ≤ n) (hN : x.regs groups ≤ N) (hM : M ≤ m ^ 2) :
        (recordLayout x M).endpoint ≤ x.regs heap + allocationSize n m N

        The actual next heap pointer advances by at most the uniform per-node allocation.