~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import 0xe6b82fa6c4c459c7023adf4b12a3ac46/LAWS.bend as LAWS

LAWS.bend -- the laws of tinygrad, stated for the Bend port.

The human states these; PROOF.bend must prove them. Each law cites the upstream tinygrad code it captures (see LAW.md for the full mapping). Only F32-free, structural facts are stated here: Bend's F32 is axiomatic, so numeric correctness is pinned by the runtime toys in tests/ instead.

2 imports
import Base
import ./tinygrad/shape.bend as Sh

Laws

law bcast_commute provedin PROOF.bendsource · line 14 · raw

@+s:List<&2, Nat> -> @+t:List<&2, Nat> -> {0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.bcast(s, t) == 0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.bcast(t, s) : List<&2, Nat>}

LAW 1 (broadcast commutes) -- tinygrad tensor.py _broadcasted: both operands are broadcast to ONE common shape; which operand came first cannot change it.

law matmul_shape provedin PROOF.bendsource · line 21 · raw

@+m:Nat -> @+k:Nat -> @+n:Nat -> {0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.matmul_out(m, k, n) == [m, n] : List<&2, Nat>}

LAW 2 (matmul shape) -- tinygrad mixin/op.py dot: (m,k) @ (k,n) = (m,n); the inner dims must agree, the output carries the outer dims.

law bcast_numel provedin PROOF.bendsource · line 32 · raw

@+s:List<&2, Nat> -> @+t:List<&2, Nat> -> @c:0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.bc(s, t) -> {0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.numel(0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.bcast(s, t)) == 0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.numel(t) : Nat}

LAW 3 (broadcast numel) -- the shape half of tinygrad's broadcast gradient rule (mixin/gradient.py: a shaped edge's gradient is summed back to its source's shape): when t dominates s, broadcasting s against t yields exactly t's element count, so summing a t-shaped gradient over the broadcast axes can restore s's shape.

law grad_accum_len provedin PROOF.bendsource · line 43 · raw

@+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> {List.length(&2, Nat, List.append(&2, Nat, xs, ys)) == Nat.add(List.length(&2, Nat, xs), List.length(&2, Nat, ys)) : Nat}

LAW 4 (gradient accumulation is lossless) -- tinygrad tensor.py backward (t.grad.assign(t.grad + g)): when a tensor is used several times, every use contributes its gradient and none is dropped; the port's gradient table accumulates a contribution list per parameter, so the invariant is that appending contributions preserves their count.

law reduce_numel provedin PROOF.bendsource · line 52 · raw

@+s:List<&2, Nat> -> {0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.numel(s) == Nat.mul(0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.at(s, 0n), 0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.numel(0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.drop_at(s, 0n))) : Nat}

LAW 6 (reduce count, axis 0) -- tinygrad mixin/reduce.py _reduce: summing over axis 0 removes dim 0, so numel(s) = dim_0(s) * numel(reduced). The general-axis form needs mul-associativity, which the port pins at runtime in tests/toy_reduce.bend instead (see LAW.md).