law partial_low

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/read.bend:285

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as K
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as S

285law partial_low:
286  for +w: U32
287  for +d: Nat
288  {K.partial(w,d) == S.low_bytes(w,Nat.min(4n,d)) : U32}