Sha3.lane_bytes: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend as Sha3
Lines 93-98 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend&start_line=93&end_line=98

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as T

# Section 4, steps 7-10: d = 256 <= r, so Z is the first 32 bytes of S.
def lane_bytes(l: T.Lane) -> List<&2, U32>:
  match l:
    case T.W{+lo, +hi}:
      [U32.and(lo, 255), U32.and(U32.shrn(lo, 8n), 255), U32.and(U32.shrn(lo, 16n), 255), U32.shrn(lo, 24n),
       U32.and(hi, 255), U32.and(U32.shrn(hi, 8n), 255), U32.and(U32.shrn(hi, 16n), 255), U32.shrn(hi, 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/keccak/types.bend&name=Lane