BatchedMatmulLAWS.batched_plan_geometry: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend as BatchedMatmulLAWS
Lines 406-417 of bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&start_line=406&end_line=417

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend as Batched

# Whatever the operands' dimensions, a plan that succeeds has PyTorch's
# output dimensions: a 1-D left operand promoted to a row and a 1-D right
# one to a column, both dropped again, and the batches broadcast
# right-aligned, an extent of 1 taking the other one's. It reads the left
# operand as its promoted extents padded with ones to rank 4, the right one
# likewise (their inner extents are equal), and the output's batch padded
# to two; these are the extents the build's layouts and
# `batched_build_logical_cells` read with.
law batched_plan_geometry:
  for +left: List<&2, U32>
  for +right: List<&2, U32>
  torch_geometry(Shape.naturals(left), Shape.naturals(right), Batched.plan_dims(left, right))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=plan_dims
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=torch_geometry
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=geometry_ops