law tail_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha3/conformance.bend:119

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha3/core.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend as F

119law tail_correct:
120  for +q: Nat
121  {C.tail(q) == F.padding_bytes(q) : List<&2, U32>}