Documentation

Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Pruned.Root

Initialization of the actual root stack frame #

Main results #

The count comes from the preceding native deduplication. The frame words are ordinary stores, not an externally supplied traversal certificate.

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

Registers assigned after the actual root query list has been computed.

Instances For
    source
    @[instance_reducible]
    instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableRootFinishLocal (i : Fin registers) :
    Decidable (RootFinishLocal i)
    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_rootFinish {w : ℕ} (x : WordRAM.Data registers) (h0 : x.regs nil = 0) (h1 : x.regs one = 1) (hw : WordRAM.Fits w (x.regs frames + 3)) :
    ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w rootFinish x y 11 ∧ y.regs level = 0 ∧ y.regs mode = 0 ∧ y.regs active = 1 ∧ y.mem = Function.update (Function.update (Function.update (Function.update x.mem (x.regs frames) (x.regs childCount)) (x.regs frames + 1) 0) (x.regs frames + 2) 1) (x.regs frames + 3) 0 ∧ WordRAM.Modifies { base := x.regs frames, length := 4 }.footprint x.mem y.mem ∧ ∀ (i : Fin registers), ¬RootFinishLocal i → y.regs i = x.regs i

    Eleven native instructions write the root's computed count, zero prefix, unit stride and zero term, then set the controller to its entry phase.

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

    Registers written by root-list construction and its first frame initialization.

    Instances For
      source
      @[instance_reducible]
      instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableRootLocal (i : Fin registers) :
      Decidable (RootLocal i)
      source
      theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_rootList {w N capacity : ℕ} (x : WordRAM.Data registers) (input : ℕ → ℕ) (hN : x.regs queryCount = N) (hinput : ∀ i < N, x.mem (x.regs queries + i) = input i) (hcodes : ∀ i < N, input i < capacity) (hsep : x.regs lists + capacity ≤ x.regs stamps) (hsrcOut : x.regs queries + N ≤ x.regs lists) (hframeList : x.regs frames + 4 ≤ x.regs lists) (hsrcFrame : x.regs queries + N ≤ x.regs frames) (hmarks : ∀ q < capacity, x.mem (x.regs stamps + q) ≤ x.regs epoch) (h0 : x.regs nil = 0) (h1 : x.regs one = 1) (h10 : x.regs ten = 10) (h9 : x.regs nine = 9) (hw : WordRAM.Fits w (x.regs queries + N + x.regs lists + capacity + x.regs stamps + capacity + N + capacity + x.regs epoch + x.regs frames + 16)) :
      ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w rootList x y (20 * N + 19) ∧ y.regs level = 0 ∧ y.regs mode = 0 ∧ y.regs active = 1 ∧ y.regs epoch = x.regs epoch + 1 ∧ ScanMemory y.mem (x.regs lists) (x.regs stamps) (x.regs epoch + 1) capacity (Finset.image input (Finset.range N)) ∧ y.mem (x.regs frames) = (Finset.image input (Finset.range N)).card ∧ y.mem (x.regs frames + 1) = 0 ∧ y.mem (x.regs frames + 2) = 1 ∧ y.mem (x.regs frames + 3) = 0 ∧ (∀ i < N, y.mem (x.regs queries + i) = input i) ∧ (∀ (a : ℕ), ¬{ base := x.regs lists, length := capacity }.Owns a → ¬{ base := x.regs stamps, length := capacity }.Owns a → ¬{ base := x.regs frames, length := 4 }.Owns a → y.mem a = x.mem a) ∧ ∀ (i : Fin registers), ¬RootLocal i → y.regs i = x.regs i

      Construct the actual distinct root list and frame. Repeated input queries are read and removed by the native timestamp scan, rather than supplied as a mathematical set. The frame, list and timestamp intervals are the only possible memory writes.