Documentation

Complexity.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Pruned.AccumulateStep

Actual native selection and accumulation of one query #

Main results #

The child-value memory premise is needed only for selected queries. Unselected child-directory cells may contain arbitrary prior values and are never loaded by the program.

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

Registers changed by selected signed accumulation or its unselected no-op.

Instances For
    source
    @[instance_reducible]
    instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableAccumulateDispatchLocal (i : Fin registers) :
    Decidable (AccumulateDispatchLocal i)
    source
    theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_accumulateDispatch {w : ℕ} {a b : ℤ} (ha : GenericRAM.Signed.Fits w a) (hb : GenericRAM.Signed.Fits w b) (x : WordRAM.Data registers) (q : ℕ) (hq : x.regs query = q) (hd : x.regs digit = q % 10) (h9 : x.regs nine = 9) (h10 : x.regs ten = 10) (hleft : selected true (x.regs term) q → x.mem (x.regs valueBase + q) = WordRAM.Signed.encode a) (hright : selected true (x.regs term) q → x.mem (x.regs childValues + q / 10) = WordRAM.Signed.encode b) (hp : WordRAM.Fits (w + 2) (x.regs valueBase + q)) (hc : WordRAM.Fits (w + 2) (x.regs childValues + q / 10)) :
    ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin (w + 2) accumulateDispatch x y 25 ∧ (y.mem = if selected true (x.regs term) q then Function.update x.mem (x.regs valueBase + q) (WordRAM.Signed.encode (a + b)) else x.mem) ∧ ∀ (i : Fin registers), ¬AccumulateDispatchLocal i → y.regs i = x.regs i

    Exactly the contributing parent queries load and add a child value. Selection is proved from the actual comparisons with digit nine and the current term register.

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

    Registers changed by loading, dispatching and advancing one parent query.

    Instances For
      source
      @[instance_reducible]
      instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableAccumulateStepLocal (i : Fin registers) :
      Decidable (AccumulateStepLocal i)
      source
      theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_accumulateStep {w : ℕ} {a b : ℤ} (ha : GenericRAM.Signed.Fits w a) (hb : GenericRAM.Signed.Fits w b) (x : WordRAM.Data registers) (q : ℕ) (hq : x.mem (x.regs listBase + x.regs index) = q) (h1 : x.regs one = 1) (h9 : x.regs nine = 9) (h10 : x.regs ten = 10) (hleft : selected true (x.regs term) q → x.mem (x.regs valueBase + q) = WordRAM.Signed.encode a) (hright : selected true (x.regs term) q → x.mem (x.regs childValues + q / 10) = WordRAM.Signed.encode b) (h10fit : WordRAM.Fits (w + 2) 10) (hr : WordRAM.Fits (w + 2) (x.regs listBase + x.regs index)) (hp : WordRAM.Fits (w + 2) (x.regs valueBase + q)) (hc : WordRAM.Fits (w + 2) (x.regs childValues + q / 10)) (hi : WordRAM.Fits (w + 2) (x.regs index + 1)) :
      ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin (w + 2) accumulateStep x y 29 ∧ y.regs index = x.regs index + 1 ∧ (y.mem = if selected true (x.regs term) q then Function.update x.mem (x.regs valueBase + q) (WordRAM.Signed.encode (a + b)) else x.mem) ∧ ∀ (i : Fin registers), ¬AccumulateStepLocal i → y.regs i = x.regs i

      One complete native parent-query iteration, including every index/digit/control operation. The conditional memory hypotheses reflect only which child words are actually requested.