Chacha8rand.double_round: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend as Chacha8rand
Lines 71-84 of bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend&start_line=71&end_line=84

import Base

# RFC 8439 2.3 inner_block (on the sixteen words of a state)
def double_round(x: List<&2, U32>) -> List<&2, U32>:
  match x:
    case [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]:
      y1 = quarter([x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15], 0n, 4n, 8n, 12n)
      y2 = quarter(y1, 1n, 5n, 9n, 13n)
      y3 = quarter(y2, 2n, 6n, 10n, 14n)
      y4 = quarter(y3, 3n, 7n, 11n, 15n)
      y5 = quarter(y4, 0n, 5n, 10n, 15n)
      y6 = quarter(y5, 1n, 6n, 11n, 12n)
      y7 = quarter(y6, 2n, 7n, 8n, 13n)
      quarter(y7, 3n, 4n, 9n, 14n)
    case _:
      x

Uses (3):
  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=bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend&name=quarter