Charged consumption of a returned child value #
Main results #
PrunedQuery.exec_addValue: compute the child suffix address, load both signed words, call the existing signed-add kernel, and store the sum at the parent query address.
The instruction bound includes all indexed accesses and the native arithmetic kernel.
def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.AddValueLocal (i : Fin registers) :
The signed workspace and two address-calculation registers used by one accumulation.
Instances For
@[instance_reducible]
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_addValue {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) (h10 : x.regs ten = 10) (hleft : x.mem (x.regs valueBase + q) = WordRAM.Signed.encode a) (hright : 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) addValue x y 22 ∧ y.mem = Function.update x.mem (x.regs valueBase + q) (WordRAM.Signed.encode (a + b)) ∧ ∀ (i : Fin registers), ¬AddValueLocal i → y.regs i = x.regs i
All twenty-two instructions are native standard-basis operations. Both operands must fit the source signed width; their sum is computed exactly by the existing two-extra-bit kernel.