Core.bytes: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/core.bend as Core
Lines 140-144 of bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/core.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/core.bend&start_line=140&end_line=144

import Base

# The 64 little-endian bytes of a state.
def bytes(s: State) -> List<&2, U32>:
  match s:
    case S{+x0,+x1,+x2,+x3,+x4,+x5,+x6,+x7,+x8,+x9,+x10,+x11,+x12,+x13,+x14,+x15}:
      [U32.and(x0,255), U32.and(U32.shrn(x0,8n),255), U32.and(U32.shrn(x0,16n),255), U32.shrn(x0,24n), U32.and(x1,255), U32.and(U32.shrn(x1,8n),255), U32.and(U32.shrn(x1,16n),255), U32.shrn(x1,24n), U32.and(x2,255), U32.and(U32.shrn(x2,8n),255), U32.and(U32.shrn(x2,16n),255), U32.shrn(x2,24n), U32.and(x3,255), U32.and(U32.shrn(x3,8n),255), U32.and(U32.shrn(x3,16n),255), U32.shrn(x3,24n), U32.and(x4,255), U32.and(U32.shrn(x4,8n),255), U32.and(U32.shrn(x4,16n),255), U32.shrn(x4,24n), U32.and(x5,255), U32.and(U32.shrn(x5,8n),255), U32.and(U32.shrn(x5,16n),255), U32.shrn(x5,24n), U32.and(x6,255), U32.and(U32.shrn(x6,8n),255), U32.and(U32.shrn(x6,16n),255), U32.shrn(x6,24n), U32.and(x7,255), U32.and(U32.shrn(x7,8n),255), U32.and(U32.shrn(x7,16n),255), U32.shrn(x7,24n), U32.and(x8,255), U32.and(U32.shrn(x8,8n),255), U32.and(U32.shrn(x8,16n),255), U32.shrn(x8,24n), U32.and(x9,255), U32.and(U32.shrn(x9,8n),255), U32.and(U32.shrn(x9,16n),255), U32.shrn(x9,24n), U32.and(x10,255), U32.and(U32.shrn(x10,8n),255), U32.and(U32.shrn(x10,16n),255), U32.shrn(x10,24n), U32.and(x11,255), U32.and(U32.shrn(x11,8n),255), U32.and(U32.shrn(x11,16n),255), U32.shrn(x11,24n), U32.and(x12,255), U32.and(U32.shrn(x12,8n),255), U32.and(U32.shrn(x12,16n),255), U32.shrn(x12,24n), U32.and(x13,255), U32.and(U32.shrn(x13,8n),255), U32.and(U32.shrn(x13,16n),255), U32.shrn(x13,24n), U32.and(x14,255), U32.and(U32.shrn(x14,8n),255), U32.and(U32.shrn(x14,16n),255), U32.shrn(x14,24n), U32.and(x15,255), U32.and(U32.shrn(x15,8n),255), U32.and(U32.shrn(x15,16n),255), U32.shrn(x15,24n)]

Uses (5):
  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=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shrn
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/core.bend&name=State