law block_sum

bendtorch@1.3.0.0 · LAWS.bend:315

import Base
import bendtorch@1.3.0.0/spec.bend as Spec

315# LAW (block_sum): summing a row in blocks gives the row's own sum, bit for bit. tree_sum adds a row's cells in pairs,
316# pass after pass. The GPU's loss kernels instead give each block of 2^p cells to one leaf, which sums it as a balanced
317# tree of pairs, and then run tree_sum's remaining passes over the block sums. When 2^p divides the row (a row of 2^p·k
318# cells), both build the same tree of additions (torch/spec.bend), for every p, k and number of passes r after the
319# first p: the same pairs added in the same order, so the same bits in F32. Any block size that divides the row gives
320# the row's sum, which is why the mutant that shrinks the cross-entropy's blocks to one cell survives.
321law block_sum:
322  for +p: Nat
323  for +k: Nat
324  for +r: Nat
325  {Spec.passes(Nat.add(r, p), Spec.blocks(0n, Nat.mul(Spec.pw(p), k), 0n)) == Spec.passes(r, Spec.blocks(p, k, 0n)) : List<&2, Spec.Sum>}