~/jendhub

def kept

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake2s/bytes.bend:208

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

208# The bytes at message offsets i..i+3 of one word, zeroed from offset len on.
209def kept(+w: U32, +i: Nat, +len: Nat) -> U32:
210  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)

Used by (2)