law streebog256_length

bend-osdev-hashes@0.1.0.0 · LAWS.bend:349

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-hashes@0.1.0.0/hashes.bend as Hs
import bend-osdev-hashes@0.1.0.0/streebog.bend as ST

349# Streebog-256 (RFC 6986): the digest of every state has 32 bytes
350law streebog256_length:
351  for +s: Hs.HsMdState<ST.HsStbCv>
352  {B.Octets.len(ST.HsStreebog.final256(s)) == 32n : Nat}