law sha3_256_hash_length

bend-osdev-crypto@0.1.0.0 · LAWS.bend:456

import bend-osdev-crypto@0.1.0.0/LAWS.bend as LAWS
import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/inst_sha3.bend as S3

456law sha3_256_hash_length:
457  for +o: B.Octets
458  {B.Octets.len(S3.CrSha3.sha3_256(o)) == 32n : Nat}

Uses (11)

Used by (0)

No other definition uses this definition.