LAWS.blowfish_bad_key_length: law of bend-osdev-blowfish@0.1.0.0
Import: import bend-osdev-blowfish@0.1.0.0/LAWS.bend as LAWS
Lines 24-27 of bend-osdev-blowfish@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-blowfish@0.1.0.0/LAWS.bend&start_line=24&end_line=27

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
import bend-osdev-blowfish@0.1.0.0/blowfish.bend as BF

# BEGIN GENERATED by gen/vectors.py: vectors
# a Blowfish key of 3 bytes is refused (32 bits at least)
law blowfish_bad_key_length:
  {Result.map(&2, &2, L.LcError, BF.LcBlowfishKey, Unit, k => Unit{}, BF.LcBlowfish.key(B.Octets.of_list([0, 0, 0]))) == Fail{L.LcBadKeyLength{3n}} : Result<&2, &2, L.LcError, Unit>}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.map
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-blowfish@0.1.0.0/blowfish.bend&name=LcBlowfish.key
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-blowfish@0.1.0.0/blowfish.bend&name=LcBlowfishKey
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-core@0.1.0.0/cipher_core.bend&name=LcError