Bytes.kept: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/bytes.bend as Bytes
Lines 208-210 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/bytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/bytes.bend&start_line=208&end_line=210

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend as R

# The bytes at message offsets i..i+3 of one word, zeroed from offset len on.
def kept(+w: U32, +i: Nat, +len: Nat) -> U32:
  R.word(R.keep_if(Nat.is_lt(i,len),R.byte(w,0n)),R.keep_if(Nat.is_lt(1n+i,len),R.byte(w,1n)),R.keep_if(Nat.is_lt(2n+i,len),R.byte(w,2n)),R.keep_if(Nat.is_lt(3n+i,len),R.byte(w,3n)))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  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/crypto/blake/blake2s.bend&name=byte
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend&name=keep_if
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend&name=word