BendMlLlama.groups_len: law of bend-ml-llama@0.2.1.0
Import: import bend-ml-llama@0.2.1.0/main.bend as BendMlLlama
Lines 600-606 of bend-ml-llama@0.2.1.0/main.bend: https://jend.leeeet.dev/read.txt?path=bend-ml-llama@0.2.1.0/main.bend&start_line=600&end_line=606

import Base

# LAW (groups_len): the query heads make exactly as many groups as there are key/value heads, so attention
# (which walks the groups and the columns together) pairs every group with a key/value head.
law groups_len:
  for n: Nat
  for +g: Nat
  for +hs: List<&2, Head>
  {List.length(&2, List<&2, Head>, groups(n, g, hs)) == n : Nat}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.drop
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-ml-llama@0.2.1.0/main.bend&name=Head
  https://jend.leeeet.dev/definition.txt?path=bend-ml-llama@0.2.1.0/main.bend&name=groups