Documentation

Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Pruned.Frame

Native stack layout and frame loading #

Main results #

Every index multiplication, pointer addition and load is an ordinary charged instruction.

source
def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.LocateLocal (i : Fin registers) :
Prop

Exactly the registers used to locate the concrete workspace regions.

Instances For
    source
    @[instance_reducible]
    instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableLocateLocal (i : Fin registers) :
    Decidable (LocateLocal i)
    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_locate {w : ℕ} (x : WordRAM.Data registers) (h1 : x.regs one = 1) (h4 : x.regs frameWidth = 4) (hw : WordRAM.Fits w (x.regs scratch + 4 * (x.regs inputDepth + 1) + 2 * (x.regs inputDepth + 1) * x.regs span + x.regs inputDepth + 8)) :
    ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w locate x y 7 ∧ y.mem = x.mem ∧ y.regs frames = x.regs scratch ∧ y.regs lists = x.regs scratch + 4 * (x.regs inputDepth + 1) ∧ y.regs values = x.regs scratch + 4 * (x.regs inputDepth + 1) + (x.regs inputDepth + 1) * x.regs span ∧ y.regs stamps = x.regs scratch + 4 * (x.regs inputDepth + 1) + 2 * (x.regs inputDepth + 1) * x.regs span ∧ ∀ (i : Fin registers), ¬LocateLocal i → y.regs i = x.regs i

    The seven actual instructions compute the workspace partition from depth and array size.

    source
    def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.LoadFrameLocal (i : Fin registers) :
    Prop

    Registers written while loading one stack frame and computing the two depth rows.

    Instances For
      source
      @[instance_reducible]
      instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableLoadFrameLocal (i : Fin registers) :
      Decidable (LoadFrameLocal i)
      source
      theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_loadFrame {w : ℕ} (x : WordRAM.Data registers) (h1 : x.regs one = 1) (h4 : x.regs frameWidth = 4) (hw : WordRAM.Fits w (x.regs frames + 4 * (x.regs level + 1) + x.regs lists + x.regs values + (x.regs level + 1) * x.regs span + x.regs level + 8)) :
      ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w loadFrame x y 17 ∧ y.mem = x.mem ∧ y.regs frame = x.regs frames + 4 * x.regs level ∧ y.regs count = x.mem (x.regs frames + 4 * x.regs level) ∧ y.regs leafPrefix = x.mem (x.regs frames + 4 * x.regs level + 1) ∧ y.regs stride = x.mem (x.regs frames + 4 * x.regs level + 2) ∧ y.regs term = x.mem (x.regs frames + 4 * x.regs level + 3) ∧ y.regs listBase = x.regs lists + x.regs level * x.regs span ∧ y.regs valueBase = x.regs values + x.regs level * x.regs span ∧ y.regs nextLevel = x.regs level + 1 ∧ y.regs childList = x.regs lists + (x.regs level + 1) * x.regs span ∧ y.regs childValues = x.regs values + (x.regs level + 1) * x.regs span ∧ ∀ (i : Fin registers), ¬LoadFrameLocal i → y.regs i = x.regs i

      Seventeen native instructions load the four words at the computed frame address and locate the current and child rows. The memory words are read, not supplied as frame arguments.