LAWS.block_sum: law of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/LAWS.bend as LAWS
Lines 315-325 of bendtorch@1.3.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/LAWS.bend&start_line=315&end_line=325

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

# 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,
# 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
# 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
# cells), both build the same tree of additions (torch/spec.bend), for every p, k and number of passes r after the
# first p: the same pairs added in the same order, so the same bits in F32. Any block size that divides the row gives
# the row's sum, which is why the mutant that shrinks the cross-entropy's blocks to one cell survives.
law block_sum:
  for +p: Nat
  for +k: Nat
  for +r: Nat
  {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>}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=blocks_passes
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=passes_add
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/spec.bend&name=Sum
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/spec.bend&name=blocks
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/spec.bend&name=passes
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/spec.bend&name=pw