There is almost no sensible description yet, but
it typechecks and implements blocked matmul and
the proof that blcoking is correct.