bend-osdev-crypto

Releases (1):
  0.1.0.0  0x01313a4f070f7ffd2bd276fcd2143eda  indexed  https://jend.leeeet.dev/files.txt?path=bend-osdev-crypto@0.1.0.0

Definitions (678, 1 to 100 shown):
  LAWS.xor_involution (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=xor_involution)
   # the cipher is its own inverse: from one state, applied twice, the data
   # comes back
   law xor_involution:
     for ~S: Data
     for ~next: S -> St.CrKsStep<S>
     for +s: S
     for +m: B.Octets
     {St.CrXor.out_data(~S, St.CrXor.update(~S, ~next, s, St.CrXor.out_data(~S, St.CrXor.update(~S, ~next, s, m)))) == m : B.Octets}
  LAWS.xor_streaming_data (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=xor_streaming_data)
   # data in pieces: the output of a ++ b is the output of a, then the output of
   # b from the state after a
   law xor_streaming_data:
     for ~S: Data
     for ~next: S -> St.CrKsStep<S>
     for +s: S
     for +a: B.Octets
     for +b: B.Octets
     {St.CrXor.out_data(~S, St.CrXor.update(~S, ~next, s, B.Octets.append(a, b))) == B.Octets.append(St.CrXor.out_data(~S, St.CrXor.update(~S, ~next, s, a)), St.CrXor.out_data(~S, St.CrXor.update(~S, ~next, St.CrXor.out_state(~S, St.CrXor.update(~S, ~next, s, a)), b))) : B.Octets}
  LAWS.xor_streaming_state (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=xor_streaming_state)
   law xor_streaming_state:
     for ~S: Data
     for ~next: S -> St.CrKsStep<S>
     for +s: S
     for +a: B.Octets
     for +b: B.Octets
     {St.CrXor.out_state(~S, St.CrXor.update(~S, ~next, s, B.Octets.append(a, b))) == St.CrXor.out_state(~S, St.CrXor.update(~S, ~next, St.CrXor.out_state(~S, St.CrXor.update(~S, ~next, s, a)), b)) : S}
  LAWS.ctr_involution (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=ctr_involution)
   law ctr_involution:
     for ~K: Data
     for ~Blk: Data
     for ~enc: K -> Blk -> Blk
     for ~blk_of: B.Octets -> Maybe<&2, Blk>
     for ~blk_to: Blk -> B.Octets
     for +s: Md.CrCtrState<K>
     for +m: B.Octets
     {St.CrXor.out_data(~Md.CrCtrState<K>, Md.CrCtr.update(~K, ~Blk, ~enc, ~blk_of, ~blk_to, s, St.CrXor.out_data(~Md.CrCtrState<K>, Md.CrCtr.update(~K, ~Blk, ~enc, ~blk_of, ~blk_to, s, m)))) == m : B.Octets}
  LAWS.ctr_streaming_data (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=ctr_streaming_data)
   law ctr_streaming_data:
     for ~K: Data
     for ~Blk: Data
     for ~enc: K -> Blk -> Blk
     for ~blk_of: B.Octets -> Maybe<&2, Blk>
     for ~blk_to: Blk -> B.Octets
     for +s: Md.CrCtrState<K>
     for +a: B.Octets
     for +b: B.Octets
     {St.CrXor.out_data(~Md.CrCtrState<K>, Md.CrCtr.update(~K, ~Blk, ~enc, ~blk_of, ~blk_to, s, B.Octets.append(a, b))) == B.Octets.append(St.CrXor.out_data(~Md.CrCtrState<K>, Md.CrCtr.update(~K, ~Blk, ~enc, ~blk_of, ~blk_to, s, a)), St.CrXor.out_data(~Md.CrCtrState<K>, Md.CrCtr.update(~K, ~Blk, ~enc, ~blk_of, ~blk_to, St.CrXor.out_state(~Md.CrCtrState<K>, Md.CrCtr.update(~K, ~Blk, ~enc, ~blk_of, ~blk_to, s, a)), b))) : B.Octets}
  LAWS.ctr_streaming_state (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=ctr_streaming_state)
   law ctr_streaming_state:
     for ~K: Data
     for ~Blk: Data
     for ~enc: K -> Blk -> Blk
     for ~blk_of: B.Octets -> Maybe<&2, Blk>
     for ~blk_to: Blk -> B.Octets
     for +s: Md.CrCtrState<K>
     for +a: B.Octets
     for +b: B.Octets
     {St.CrXor.out_state(~Md.CrCtrState<K>, Md.CrCtr.update(~K, ~Blk, ~enc, ~blk_of, ~blk_to, s, B.Octets.append(a, b))) == St.CrXor.out_state(~Md.CrCtrState<K>, Md.CrCtr.update(~K, ~Blk, ~enc, ~blk_of, ~blk_to, St.CrXor.out_state(~Md.CrCtrState<K>, Md.CrCtr.update(~K, ~Blk, ~enc, ~blk_of, ~blk_to, s, a)), b)) : Md.CrCtrState<K>}
  LAWS.cmblock_format (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=cmblock_format)
   law cmblock_format:
     for +b: M.CmBlock
     {CM.CrBlk128.of_octets(CM.CrBlk128.to_octets(b)) == Some{b} : Maybe<&2, M.CmBlock>}
  LAWS.cmblock_xor (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=cmblock_xor)
   law cmblock_xor:
     for a: M.CmBlock
     for b: M.CmBlock
     {CM.CrBlk128.xor(CM.CrBlk128.xor(a, b), b) == a : M.CmBlock}
  LAWS.lcblock64_format (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=lcblock64_format)
   law lcblock64_format:
     for +b: L.LcBlock64
     {L.LcBlock64.of_octets(L.LcBlock64.to_octets(b)) == Some{b} : Maybe<&2, L.LcBlock64>}
  LAWS.lcblock64_xor (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=lcblock64_xor)
   law lcblock64_xor:
     for a: L.LcBlock64
     for b: L.LcBlock64
     {LC.CrBlk64.xor(LC.CrBlk64.xor(a, b), b) == a : L.LcBlock64}
  LAWS.mac_verify_tag_accepts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=mac_verify_tag_accepts)
   law mac_verify_tag_accepts:
     for ~K: Data
     for ~compute: K -> B.Octets -> B.Octets
     for +k: K
     for +m: B.Octets
     {Mc.CrMac.verify_tag(~K, ~compute, k, m, compute(k, m)) == True{} : Bool}
  LAWS.mac_verify_tag_agrees (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=mac_verify_tag_agrees)
   law mac_verify_tag_agrees:
     for ~K: Data
     for ~compute: K -> B.Octets -> B.Octets
     for +k: K
     for +m: B.Octets
     for t: B.Octets
     {Mc.CrMac.verify_tag(~K, ~compute, k, m, t) == B.Octets.is_eq(compute(k, m), t) : Bool}
  LAWS.hmac_accepts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=hmac_accepts)
   law hmac_accepts:
     for ~digest: B.Octets -> B.Octets
     for +kk: Hm.CrHmacKey
     for +m: B.Octets
     {Hm.CrHmac.verify(~digest, kk, m, Hm.CrHmac.mac(~digest, kk, m)) == True{} : Bool}
  LAWS.cmac_accepts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=cmac_accepts)
   law cmac_accepts:
     for ~K: Data
     for ~enc: K -> M.CmBlock -> M.CmBlock
     for +k: K
     for +m: B.Octets
     {CMI.CrCmac.verify(~K, ~enc, k, m, CMI.CrCmac.mac(~K, ~enc, k, m)) == True{} : Bool}
  LAWS.xcbc_accepts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=xcbc_accepts)
   # XCBC-MAC over every block cipher (xcbc.bend) accepts what it computes
   law xcbc_accepts:
     for ~K: Data
     for ~Blk: Data
     for ~bsize: Nat
     for ~enc: K -> Blk -> Blk
     for ~blk_of: B.Octets -> Maybe<&2, Blk>
     for ~blk_to: Blk -> B.Octets
     for +kk: Xc.CrXcbcKey<K>
     for +m: B.Octets
     {Xc.CrXcbc.verify(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, kk, m, Xc.CrXcbc.mac(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, kk, m)) == True{} : Bool}
  LAWS.vmac_accepts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=vmac_accepts)
   # VMAC over every block cipher and nonce length (vmac.bend) accepts what it
   # computes
   law vmac_accepts:
     for ~K: Data
     for ~Blk: Data
     for ~bsize: Nat
     for ~enc: K -> Blk -> Blk
     for ~blk_of: B.Octets -> Maybe<&2, Blk>
     for ~blk_to: Blk -> B.Octets
     for ~nlen: Nat
     for +kk: Vm.CrVmacKey<K>
     …
  LAWS.crc32_hash_streaming (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=crc32_hash_streaming)
   law crc32_hash_streaming:
     for ~spec: C.Crc32Spec
     for c: U32
     for +a: B.Octets
     for +b: B.Octets
     {CR.CrCrc32.update(~spec, c, B.Octets.append(a, b)) == CR.CrCrc32.update(~spec, CR.CrCrc32.update(~spec, c, a), b) : U32}
  LAWS.crc32_hash_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=crc32_hash_split)
   law crc32_hash_split:
     for ~spec: C.Crc32Spec
     for +a: B.Octets
     for +b: B.Octets
     {CR.CrCrc32.final(~spec, CR.CrCrc32.update(~spec, CR.CrCrc32.update(~spec, CR.CrCrc32.init(~spec), a), b)) == CR.CrCrc32.digest(~spec, B.Octets.append(a, b)) : B.Octets}
  LAWS.crc64_hash_streaming (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=crc64_hash_streaming)
   law crc64_hash_streaming:
     for ~spec: C.Crc64Spec
     for c: W.W64
     for +a: B.Octets
     for +b: B.Octets
     {CR.CrCrc64.update(~spec, c, B.Octets.append(a, b)) == CR.CrCrc64.update(~spec, CR.CrCrc64.update(~spec, c, a), b) : W.W64}
  LAWS.crc64_hash_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=crc64_hash_split)
   law crc64_hash_split:
     for ~spec: C.Crc64Spec
     for +a: B.Octets
     for +b: B.Octets
     {CR.CrCrc64.final(~spec, CR.CrCrc64.update(~spec, CR.CrCrc64.update(~spec, CR.CrCrc64.init(~spec), a), b)) == CR.CrCrc64.digest(~spec, B.Octets.append(a, b)) : B.Octets}
  LAWS.lift_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=lift_round_trip)
   law lift_round_trip:
     for ~E: Data
     for ~f: E -> Cr.CrError
     for d: B.Octets -> Result<&2, &2, E, B.Octets>
     for r: Result<&2, &2, E, B.Octets>
     for +p: B.Octets
     for h: {Result.bind(&2, &2, E, B.Octets, B.Octets, r, d) == Result.map(&2, &2, E, B.Octets, B.Octets, c => p, r) : Result<&2, &2, E, B.Octets>}
     {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, Cr.CrError.lift(~E, ~B.Octets, ~f, r), c => Cr.CrError.lift(~E, ~B.Octets, ~f, d(c))) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, Cr.CrError.lift(~E, ~B.Octets, ~f, r)) : Result<&2, &2, Cr.CrError, B.Octets>}
  LAWS.ccm_round_trip_if (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=ccm_round_trip_if)
   # CCM as an AEAD (inst_ccm.bend), for every 128-bit block cipher, key, tag
   # length, nonce, associated data and message: the AEAD round trip, given
   # cipher-modes' ccm_round_trip at the same arguments (h). cipher-modes
   # proves h for every input, but a proof that imports its PROOF.bend fails
   # --verdict (its laws with a template hypothesis), so the two are joined in
   # README.md, not here.
   law ccm_round_trip_if:
     for ~K: Data
     for ~enc: K -> M.CmBlock -> M.CmBlock
     for ~tlen: Nat
     for +k: K
     …
  LAWS.sign_verify_bytes_if (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sign_verify_bytes_if)
   # Signatures and key agreement (sign.bend, kex.bend): the generic helpers
   # keep the interface laws (README.md); the instances (RSA, DH, ECDSA, ECDH,
   # SM2, EC-RDSA) and their laws are in bend-osdev-pubkey. A signature
   # checked from the public key's bytes is accepted, for every scheme, secret
   # key and message, when the scheme's pk_format and accepts laws hold there
   # (hf, ha)
   law sign_verify_bytes_if:
     for ~SK: Data
     for ~PK: Data
     for ~public: SK -> PK
     for ~pk_of: B.Octets -> Result<&2, &2, Cr.CrError, PK>
     …
  LAWS.kex_agree_if (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=kex_agree_if)
   # two parties agree from each other's public-key bytes, for every scheme and
   # pair of secret keys, when the keys parse (hx, hy), the public keys survive
   # their bytes (hfx, hfy) and the scheme's agree law holds for them (h)
   law kex_agree_if:
     for ~SK: Data
     for ~PK: Data
     for ~secret: B.Octets -> Result<&2, &2, Cr.CrError, SK>
     for ~public: SK -> PK
     for ~pk_of: B.Octets -> Result<&2, &2, Cr.CrError, PK>
     for ~pk_to: PK -> B.Octets
     for ~shared: SK -> PK -> Result<&2, &2, Cr.CrError, B.Octets>
     …
  LAWS.crc32_hash_check (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=crc32_hash_check)
   law crc32_hash_check:
     {CR.CrCrc32.digest(~C.crc32.spec(), B.Octets.of_string("123456789")) == B.Octets.of_list([203, 244, 57, 38]) : B.Octets}
  LAWS.crc32c_hash_check (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=crc32c_hash_check)
   law crc32c_hash_check:
     {CR.CrCrc32.digest(~C.crc32c.spec(), B.Octets.of_string("123456789")) == B.Octets.of_list([227, 6, 146, 131]) : B.Octets}
  LAWS.crc64_xz_hash_check (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=crc64_xz_hash_check)
   law crc64_xz_hash_check:
     {CR.CrCrc64.digest(~C.crc64_xz.spec(), B.Octets.of_string("123456789")) == B.Octets.of_list([153, 93, 201, 187, 223, 25, 57, 250]) : B.Octets}
  LAWS.crc32_hash_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=crc32_hash_length)
   # a CRC-32 digest is 4 bytes, for every parameter set and register
   law crc32_hash_length:
     for ~spec: C.Crc32Spec
     for c: U32
     {B.Octets.len(CR.CrCrc32.final(~spec, c)) == 4n : Nat}
  LAWS.hmac_crc32_vector (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=hmac_crc32_vector)
   # HMAC over CRC-32 (the key "key", the message "The quick brown fox"): the
   # value of Python's hmac module over binascii.crc32 (ref/gen.py checks the
   # same construction on random keys and messages)
   law hmac_crc32_vector:
     {Hm.CrHmac.mac(~CR.CrCrc32.digest(~C.crc32.spec()), Hm.CrHmac.key(~64n, ~CR.CrCrc32.digest(~C.crc32.spec()), B.Octets.of_string("key")), B.Octets.of_string("The quick brown fox")) == B.Octets.of_list([69, 52, 205, 87]) : B.Octets}
  LAWS.rc4_empty_key (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=rc4_empty_key)
   # refusals: an RC4 key of 0 bytes, an IV given to RC4, a CTR counter block
   # of the wrong length, bytes that are not whole blocks, and an HKDF output
   # longer than 255 digests
   law rc4_empty_key:
     {Result.map(&2, &2, Cr.CrError, R.LcRc4State, Unit, s => Unit{}, RC.CrRc4.start(B.Octets.empty(), B.Octets.empty())) == Fail{Cr.CrBadKeyLength{0n}} : Result<&2, &2, Cr.CrError, Unit>}
  LAWS.rc4_iv_refused (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=rc4_iv_refused)
   law rc4_iv_refused:
     {Result.map(&2, &2, Cr.CrError, R.LcRc4State, Unit, s => Unit{}, RC.CrRc4.start(B.Octets.empty(), B.Octets.zeros(1n))) == Fail{Cr.CrBadIvLength{1n}} : Result<&2, &2, Cr.CrError, Unit>}
  LAWS.ctr_bad_iv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=ctr_bad_iv)
   law ctr_bad_iv:
     {Result.map(&2, &2, Cr.CrError, Md.CrCtrState<D.LcDesKey>, Unit, s => Unit{}, Md.CrCtr.start(~D.LcDesKey, ~8n, ~LC.CrLc.key(~D.LcDesKey, ~D.LcDes.key), B.Octets.zeros(8n), B.Octets.zeros(7n))) == Fail{Cr.CrBadIvLength{7n}} : Result<&2, &2, Cr.CrError, Unit>}
  LAWS.blocks_of_not_whole (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=blocks_of_not_whole)
   law blocks_of_not_whole:
     {Result.map(&2, &2, Cr.CrError, List<&2, L.LcBlock64>, Unit, bs => Unit{}, Md.CrModes.blocks_of(~L.LcBlock64, ~8n, ~L.LcBlock64.of_octets, B.Octets.zeros(12n))) == Fail{Cr.CrNotBlockMultiple{12n}} : Result<&2, &2, Cr.CrError, Unit>}
  LAWS.hkdf_too_long (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=hkdf_too_long)
   law hkdf_too_long:
     {Result.map(&2, &2, Cr.CrError, B.Octets, Unit, o => Unit{}, Hk.CrHkdf.derive(~64n, ~4n, ~CR.CrCrc32.digest(~C.crc32.spec()), B.Octets.of_string("ikm"), B.Octets.empty(), B.Octets.empty(), 1021n)) == Fail{Cr.CrBadOutputLength{1021n}} : Result<&2, &2, Cr.CrError, Unit>}
  LAWS.aes_fips197_c1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=aes_fips197_c1)
   # FIPS 197 Appendix C.1 through the block-cipher interface: AES-128, its
   # encryption key schedule then one block of bytes (with CrAes.key, which
   # computes the decryption round keys too, the vector checks but runs past
   # --verdict's kernel; check.bend runs it both ways)
   law aes_fips197_c1:
     {Bk.CrBlockCipher.encrypt_with(~X.CmAesKey, ~M.CmBlock, ~A.CrAes.key_enc, ~X.CmAes.encrypt, ~CM.CrBlk128.of_octets, ~CM.CrBlk128.to_octets, B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([0, 17, 34, 51, 68, 85, 102, 119, 136, 153, 170, 187, 204, 221, 238, 255])) == Done{B.Octets.of_list([105, 196, 224, 216, 106, 123, 4, 48, 216, 205, 183, 128, 112, 180, 197, 90])} : Result<&2, &2, Cr.CrError, B.Octets>}
  LAWS.crc32_hash_split3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=crc32_hash_split3)
   law crc32_hash_split3:
     for ~spec: C.Crc32Spec
     for +a: B.Octets
     for +b: B.Octets
     for +c: B.Octets
     {CR.CrCrc32.final(~spec, CR.CrCrc32.update(~spec, CR.CrCrc32.update(~spec, CR.CrCrc32.update(~spec, CR.CrCrc32.init(~spec), a), b), c)) == CR.CrCrc32.digest(~spec, B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
  LAWS.crc64_hash_split3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=crc64_hash_split3)
   law crc64_hash_split3:
     for ~spec: C.Crc64Spec
     for +a: B.Octets
     for +b: B.Octets
     for +c: B.Octets
     {CR.CrCrc64.final(~spec, CR.CrCrc64.update(~spec, CR.CrCrc64.update(~spec, CR.CrCrc64.update(~spec, CR.CrCrc64.init(~spec), a), b), c)) == CR.CrCrc64.digest(~spec, B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
  LAWS.sha256_spec (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha256_spec)
   law sha256_spec:
     for +o: B.Octets
     {SH.CrSha2.sha256(o) == B.Octets.of_list(F256.sha256_bytes(B.Octets.to_list(o))) : B.Octets}
  LAWS.sha256_hash_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha256_hash_split)
   law sha256_hash_split:
     for +a: B.Octets
     for +b: B.Octets
     {SH.CrSha2.final(SH.CrSha2.update(SH.CrSha2.update(SH.CrSha2.init256(), a), b)) == SH.CrSha2.sha256(B.Octets.append(a, b)) : B.Octets}
  LAWS.sha256_hash_split3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha256_hash_split3)
   law sha256_hash_split3:
     for +a: B.Octets
     for +b: B.Octets
     for +c: B.Octets
     {SH.CrSha2.final(SH.CrSha2.update(SH.CrSha2.update(SH.CrSha2.update(SH.CrSha2.init256(), a), b), c)) == SH.CrSha2.sha256(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
  LAWS.sha256_hash_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha256_hash_length)
   law sha256_hash_length:
     for +o: B.Octets
     {B.Octets.len(SH.CrSha2.sha256(o)) == 32n : Nat}
  LAWS.sha512_spec (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha512_spec)
   law sha512_spec:
     for +o: B.Octets
     {SH.CrSha2.sha512(o) == B.Octets.of_list(F512.sha512_bytes(B.Octets.to_list(o))) : B.Octets}
  LAWS.sha512_hash_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha512_hash_split)
   law sha512_hash_split:
     for +a: B.Octets
     for +b: B.Octets
     {SH.CrSha2.final(SH.CrSha2.update(SH.CrSha2.update(SH.CrSha2.init512(), a), b)) == SH.CrSha2.sha512(B.Octets.append(a, b)) : B.Octets}
  LAWS.sha512_hash_split3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha512_hash_split3)
   law sha512_hash_split3:
     for +a: B.Octets
     for +b: B.Octets
     for +c: B.Octets
     {SH.CrSha2.final(SH.CrSha2.update(SH.CrSha2.update(SH.CrSha2.update(SH.CrSha2.init512(), a), b), c)) == SH.CrSha2.sha512(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
  LAWS.sha512_hash_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha512_hash_length)
   law sha512_hash_length:
     for +o: B.Octets
     {B.Octets.len(SH.CrSha2.sha512(o)) == 64n : Nat}
  LAWS.sha3_256_spec (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha3_256_spec)
   law sha3_256_spec:
     for +o: B.Octets
     {S3.CrSha3.sha3_256(o) == B.Octets.of_list(F202.sha3_256(B.Octets.to_list(o))) : B.Octets}
  LAWS.sha3_256_hash_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha3_256_hash_split)
   law sha3_256_hash_split:
     for +a: B.Octets
     for +b: B.Octets
     {S3.CrSha3.final(S3.CrSha3.update(S3.CrSha3.update(S3.CrSha3.init(), a), b)) == S3.CrSha3.sha3_256(B.Octets.append(a, b)) : B.Octets}
  LAWS.sha3_256_hash_split3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha3_256_hash_split3)
   law sha3_256_hash_split3:
     for +a: B.Octets
     for +b: B.Octets
     for +c: B.Octets
     {S3.CrSha3.final(S3.CrSha3.update(S3.CrSha3.update(S3.CrSha3.update(S3.CrSha3.init(), a), b), c)) == S3.CrSha3.sha3_256(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
  LAWS.sha3_256_hash_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha3_256_hash_length)
   law sha3_256_hash_length:
     for +o: B.Octets
     {B.Octets.len(S3.CrSha3.sha3_256(o)) == 32n : Nat}
  LAWS.hkdf_sha256_too_long (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=hkdf_sha256_too_long)
   # HKDF over SHA-256 refuses more than 255 digests (8160 bytes)
   law hkdf_sha256_too_long:
     {Result.map(&2, &2, Cr.CrError, B.Octets, Unit, o => Unit{}, Hk.CrHkdf.derive(~64n, ~32n, ~SH.CrSha2.sha256, B.Octets.of_string("ikm"), B.Octets.empty(), B.Octets.empty(), 8161n)) == Fail{Cr.CrBadOutputLength{8161n}} : Result<&2, &2, Cr.CrError, Unit>}
  LAWS.sha256_abc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha256_abc)
   # FIPS 180-4's example "abc" (NIST's SHA examples), through the hash
   # interface
   law sha256_abc:
     {SH.CrSha2.sha256(B.Octets.of_string("abc")) == B.Octets.of_list([186, 120, 22, 191, 143, 1, 207, 234, 65, 65, 64, 222, 93, 174, 34, 35, 176, 3, 97, 163, 150, 23, 122, 156, 180, 16, 255, 97, 242, 0, 21, 173]) : B.Octets}
  LAWS.sha3_256_abc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sha3_256_abc)
   # FIPS 202's SHA3-256 of "abc" (NIST's SHA-3 examples), through the hash
   # interface
   law sha3_256_abc:
     {S3.CrSha3.sha3_256(B.Octets.of_string("abc")) == B.Octets.of_list([58, 152, 93, 167, 79, 226, 37, 178, 4, 92, 23, 45, 107, 211, 144, 189, 133, 95, 8, 110, 62, 157, 82, 91, 70, 191, 226, 69, 17, 67, 21, 50]) : B.Octets}
  LAWS.hmac_sha256_rfc4231_2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=hmac_sha256_rfc4231_2)
   # RFC 4231 test case 2: HMAC-SHA-256 with the key "Jefe"
   law hmac_sha256_rfc4231_2:
     {Hm.CrHmac.mac(~SH.CrSha2.sha256, Hm.CrHmac.key(~64n, ~SH.CrSha2.sha256, B.Octets.of_string("Jefe")), B.Octets.of_string("what do ya want for nothing?")) == B.Octets.of_list([91, 220, 193, 70, 191, 96, 117, 78, 106, 4, 36, 38, 8, 149, 117, 199, 90, 0, 63, 8, 157, 39, 57, 131, 157, 236, 88, 185, 100, 236, 56, 67]) : B.Octets}
  LAWS.michael_accepts (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=michael_accepts)
   # Michael as a MAC (inst_michael.bend): it accepts what it computes, for
   # every key and message (it uses the named default verify); a key of
   # another length than 8 bytes is refused; the sixth test vector recalled as
   # IEEE 802.11i's, through the MAC interface (not checked against a published
   # copy: hashes/README.md)
   law michael_accepts:
     for +k: Hs.HsW2
     for +m: B.Octets
     {MIC.CrMichael.verify(k, m, HMI.HsMichael.mic(k, m)) == True{} : Bool}
  LAWS.michael_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=michael_key_length)
   law michael_key_length:
     {Result.map(&2, &2, Cr.CrError, Hs.HsW2, Unit, k => Unit{}, MIC.CrMichael.key(B.Octets.zeros(16n))) == Fail{Cr.CrBadKeyLength{16n}} : Result<&2, &2, Cr.CrError, Unit>}
  LAWS.michael_mac_vector (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=michael_mac_vector)
   law michael_mac_vector:
     {Mc.CrMac.compute_with(~Hs.HsW2, ~MIC.CrMichael.key, ~HMI.HsMichael.mic, B.Octets.of_list([213, 94, 16, 5, 16, 18, 137, 134]), B.Octets.of_string("Michael")) == Done{B.Octets.of_list([10, 148, 43, 18, 78, 202, 165, 70])} : Result<&2, &2, Cr.CrError, B.Octets>}
  LAWS.pbkdf2_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=pbkdf2_length)
   # PBKDF2 over any MAC (pbkdf2.bend), for every MAC, password, salt,
   # iteration count and length: a derivation that succeeds gives exactly the
   # length asked for (the KDF interface's length law); the unchecked stream
   # has that length, and a shorter stream is a prefix of a longer (the KDF
   # interface's prefix law)
   law pbkdf2_length:
     for ~K: Data
     for ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>
     for ~compute: K -> B.Octets -> B.Octets
     for ~hlen: Nat
     for +p: B.Octets
     …
  LAWS.pbkdf2_stream_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=pbkdf2_stream_length)
   law pbkdf2_stream_length:
     for ~K: Data
     for ~compute: K -> B.Octets -> B.Octets
     for +k: K
     for +salt: B.Octets
     for +c: U32
     for +n: Nat
     {B.Octets.len(Pb.CrPbkdf2.stream(~K, ~compute, k, salt, c, n)) == n : Nat}
  LAWS.pbkdf2_stream_prefix (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=pbkdf2_stream_prefix)
   law pbkdf2_stream_prefix:
     for ~K: Data
     for ~compute: K -> B.Octets -> B.Octets
     for +k: K
     for +salt: B.Octets
     for +c: U32
     for +n: Nat
     for +j: Nat
     {B.Octets.take(n, Pb.CrPbkdf2.stream(~K, ~compute, k, salt, c, Nat.add(n, j))) == Pb.CrPbkdf2.stream(~K, ~compute, k, salt, c, n) : B.Octets}
  LAWS.pbkdf2_zero_iterations (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=pbkdf2_zero_iterations)
   # PBKDF2 refuses an iteration count of 0 (over HMAC-SHA-1)
   law pbkdf2_zero_iterations:
     {Result.map(&2, &2, Cr.CrError, B.Octets, Unit, o => Unit{}, PbI.CrPbkdf2.hmac_sha1(B.Octets.of_string("password"), B.Octets.of_string("salt"), 0, 20n)) == Fail{Cr.CrTooShort{0n}} : Result<&2, &2, Cr.CrError, Unit>}
  LAWS.pbkdf2_hmac_sha1_rfc6070_1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=pbkdf2_hmac_sha1_rfc6070_1)
   # RFC 6070 test cases 1 and 2: PBKDF2-HMAC-SHA1, P = "password",
   # S = "salt", c = 1 and 2, dkLen = 20
   law pbkdf2_hmac_sha1_rfc6070_1:
     {PbI.CrPbkdf2.hmac_sha1(B.Octets.of_string("password"), B.Octets.of_string("salt"), 1, 20n) == Done{B.Octets.of_list([12, 96, 200, 15, 150, 31, 14, 113, 243, 169, 181, 36, 175, 96, 18, 6, 47, 224, 55, 166])} : Result<&2, &2, Cr.CrError, B.Octets>}
  LAWS.pbkdf2_hmac_sha1_rfc6070_2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=pbkdf2_hmac_sha1_rfc6070_2)
   law pbkdf2_hmac_sha1_rfc6070_2:
     {PbI.CrPbkdf2.hmac_sha1(B.Octets.of_string("password"), B.Octets.of_string("salt"), 2, 20n) == Done{B.Octets.of_list([234, 108, 1, 77, 199, 45, 111, 140, 205, 30, 217, 42, 206, 29, 65, 240, 216, 222, 137, 87])} : Result<&2, &2, Cr.CrError, B.Octets>}
  LAWS.pbkdf2_hmac_sha256_rfc7914_1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=pbkdf2_hmac_sha256_rfc7914_1)
   # RFC 7914, section 11: PBKDF2-HMAC-SHA256, P = "passwd", S = "salt",
   # c = 1: the first 32 of its 64 bytes (a shorter output is a prefix of a
   # longer, pbkdf2_stream_prefix; all 64 bytes, two blocks, run past
   # --verdict's kernel fuel, and check.bend computes them)
   law pbkdf2_hmac_sha256_rfc7914_1:
     {PbI.CrPbkdf2.hmac_sha256(B.Octets.of_string("passwd"), B.Octets.of_string("salt"), 1, 32n) == Done{B.Octets.of_list([85, 172, 4, 110, 86, 227, 8, 159, 236, 22, 145, 194, 37, 68, 182, 5, 249, 65, 133, 33, 109, 222, 4, 101, 230, 139, 157, 87, 194, 13, 172, 188])} : Result<&2, &2, Cr.CrError, B.Octets>}
  LAWS.kbkdf_counter_stream_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=kbkdf_counter_stream_length)
   # SP 800-108 KDFs over any MAC (kbkdf.bend), for every MAC, key, fixed
   # input data and length: each stream has the length asked for, a shorter
   # stream is a prefix of a longer one with the same fixed input (and IV), and
   # a derivation that succeeds has the length asked for. (The interface's
   # prefix law holds of the streams: a derivation binds its length L into
   # the fixed input, so derivations of two lengths differ.)
   law kbkdf_counter_stream_length:
     for ~K: Data
     for ~compute: K -> B.Octets -> B.Octets
     for ~rlen: Nat
     for +k: K
     …
  LAWS.kbkdf_counter_stream_prefix (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=kbkdf_counter_stream_prefix)
   law kbkdf_counter_stream_prefix:
     for ~K: Data
     for ~compute: K -> B.Octets -> B.Octets
     for ~rlen: Nat
     for +k: K
     for +fixed: B.Octets
     for +n: Nat
     for +j: Nat
     {B.Octets.take(n, Kb.CrKbkdf.counter_stream(~K, ~compute, ~rlen, k, fixed, Nat.add(n, j))) == Kb.CrKbkdf.counter_stream(~K, ~compute, ~rlen, k, fixed, n) : B.Octets}
  LAWS.kbkdf_feedback_stream_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=kbkdf_feedback_stream_length)
   law kbkdf_feedback_stream_length:
     for ~K: Data
     for ~compute: K -> B.Octets -> B.Octets
     for ~rlen: Nat
     for +k: K
     for +iv: B.Octets
     for +fixed: B.Octets
     for +n: Nat
     {B.Octets.len(Kb.CrKbkdf.feedback_stream(~K, ~compute, ~rlen, k, iv, fixed, n)) == n : Nat}
  LAWS.kbkdf_feedback_stream_prefix (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=kbkdf_feedback_stream_prefix)
   law kbkdf_feedback_stream_prefix:
     for ~K: Data
     for ~compute: K -> B.Octets -> B.Octets
     for ~rlen: Nat
     for +k: K
     for +iv: B.Octets
     for +fixed: B.Octets
     for +n: Nat
     for +j: Nat
     {B.Octets.take(n, Kb.CrKbkdf.feedback_stream(~K, ~compute, ~rlen, k, iv, fixed, Nat.add(n, j))) == Kb.CrKbkdf.feedback_stream(~K, ~compute, ~rlen, k, iv, fixed, n) : B.Octets}
  LAWS.kbkdf_counter_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=kbkdf_counter_length)
   law kbkdf_counter_length:
     for ~K: Data
     for ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>
     for ~compute: K -> B.Octets -> B.Octets
     for ~hlen: Nat
     for ~rlen: Nat
     for ~llen: Nat
     for +ki: B.Octets
     for +label: B.Octets
     for +context: B.Octets
     for +n: Nat
     {Result.map(&2, &2, Cr.CrError, B.Octets, Nat, o => B.Octets.len(o), Kb.CrKbkdf.counter_kdf(~K, ~key, ~compute, ~hlen, ~rlen, ~llen, ki, label, context, n)) == Result.map(&2, &2, Cr.CrError, B.Octets, Nat, o => n, Kb.CrKbkdf.counter_kdf(~K, ~key, ~compute, ~hlen, ~rlen, ~llen, ki, label, context, n)) : Result<&2, &2, Cr.CrError, Nat>}
  LAWS.kbkdf_feedback_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=kbkdf_feedback_length)
   law kbkdf_feedback_length:
     for ~K: Data
     for ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>
     for ~compute: K -> B.Octets -> B.Octets
     for ~hlen: Nat
     for ~rlen: Nat
     for ~llen: Nat
     for +ki: B.Octets
     for +iv: B.Octets
     for +label: B.Octets
     for +context: B.Octets
     …
  LAWS.kbkdf_hmac_sha256_vector (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=kbkdf_hmac_sha256_vector)
   # KBKDF in counter mode over HMAC-SHA-256 (32-bit counter and [L]_2), the
   # key "secret key bytes", Label "label", Context "context", 32 bytes:
   # Python's cryptography's KBKDFHMAC gives this value. Stated on the stream
   # (what CrKbkdf.counter_kdf returns once its length checks pass): those
   # checks compare with 2^32, which --verdict's kernel cannot compute in time;
   # check.bend runs the checked derivation
   law kbkdf_hmac_sha256_vector:
     {Kb.CrKbkdf.counter_stream(~Hm.CrHmacKey, ~Hm.CrHmac.mac(~SH.CrSha2.sha256), ~4n, Hm.CrHmac.key(~64n, ~SH.CrSha2.sha256, B.Octets.of_string("secret key bytes")), Kb.CrKbkdf.fixed(~4n, B.Octets.of_string("label"), B.Octets.of_string("context"), 32n), 32n) == B.Octets.of_list([36, 187, 186, 187, 150, 131, 248, 143, 109, 68, 1, 79, 191, 147, 235, 99, 232, 125, 99, 110, 60, 243, 238, 232, 217, 114, 189, 30, 217, 156, 9, 202]) : B.Octets}
  LAWS.des_block_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=des_block_round_trip)
   # BEGIN GENERATED by gen/instances.py: laws
   # DES (legacy-ciphers): decryption undoes encryption, for every key and block
   law des_block_round_trip:
     for k: D.LcDesKey
     for +b: L.LcBlock64
     {D.LcDes.decrypt(k, D.LcDes.encrypt(k, b)) == b : L.LcBlock64}
  LAWS.des_block_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=des_block_round_trip_dual)
   # DES (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
   law des_block_round_trip_dual:
     for k: D.LcDesKey
     for +b: L.LcBlock64
     {D.LcDes.encrypt(k, D.LcDes.decrypt(k, b)) == b : L.LcBlock64}
  LAWS.des_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=des_key_length)
   # DES (legacy-ciphers): a key of 7 bytes is refused
   law des_key_length:
     {Result.map(&2, &2, Cr.CrError, D.LcDesKey, Unit, k => Unit{}, LC.CrLc.key(~D.LcDesKey, ~D.LcDes.key, B.Octets.zeros(7n))) == Fail{Cr.CrBadKeyLength{7n}} : Result<&2, &2, Cr.CrError, Unit>}
  LAWS.des_ecb_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=des_ecb_round_trip)
   # DES (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
   law des_ecb_round_trip:
     for +k: D.LcDesKey
     for +bs: List<&2, L.LcBlock64>
     {Md.CrEcb.decrypt_blocks(~D.LcDesKey, ~L.LcBlock64, ~D.LcDes.decrypt, k, Md.CrEcb.encrypt_blocks(~D.LcDesKey, ~L.LcBlock64, ~D.LcDes.encrypt, k, bs)) == bs : List<&2, L.LcBlock64>}
  LAWS.des_cbc_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=des_cbc_round_trip)
   # DES (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
   law des_cbc_round_trip:
     for +k: D.LcDesKey
     for +iv: L.LcBlock64
     for +bs: List<&2, L.LcBlock64>
     {Md.CrCbc.decrypt_blocks(~D.LcDesKey, ~L.LcBlock64, ~D.LcDes.decrypt, ~LC.CrBlk64.xor, k, iv, Md.CrCbc.encrypt_blocks(~D.LcDesKey, ~L.LcBlock64, ~D.LcDes.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
  LAWS.des_pcbc_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=des_pcbc_round_trip)
   # DES (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
   law des_pcbc_round_trip:
     for +k: D.LcDesKey
     for +iv: L.LcBlock64
     for +bs: List<&2, L.LcBlock64>
     {Pc.CrPcbc.decrypt_blocks(~D.LcDesKey, ~L.LcBlock64, ~D.LcDes.decrypt, ~LC.CrBlk64.xor, k, iv, Pc.CrPcbc.encrypt_blocks(~D.LcDesKey, ~L.LcBlock64, ~D.LcDes.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
  LAWS.tdes_block_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=tdes_block_round_trip)
   # Triple DES (legacy-ciphers): decryption undoes encryption, for every key and block
   law tdes_block_round_trip:
     for k: T.LcTdesKey
     for +b: L.LcBlock64
     {T.LcTdes.decrypt(k, T.LcTdes.encrypt(k, b)) == b : L.LcBlock64}
  LAWS.tdes_block_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=tdes_block_round_trip_dual)
   # Triple DES (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
   law tdes_block_round_trip_dual:
     for k: T.LcTdesKey
     for +b: L.LcBlock64
     {T.LcTdes.encrypt(k, T.LcTdes.decrypt(k, b)) == b : L.LcBlock64}
  LAWS.tdes_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=tdes_key_length)
   # Triple DES (legacy-ciphers): a key of 8 bytes is refused
   law tdes_key_length:
     {Result.map(&2, &2, Cr.CrError, T.LcTdesKey, Unit, k => Unit{}, LC.CrLc.key(~T.LcTdesKey, ~T.LcTdes.key, B.Octets.zeros(8n))) == Fail{Cr.CrBadKeyLength{8n}} : Result<&2, &2, Cr.CrError, Unit>}
  LAWS.tdes_ecb_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=tdes_ecb_round_trip)
   # Triple DES (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
   law tdes_ecb_round_trip:
     for +k: T.LcTdesKey
     for +bs: List<&2, L.LcBlock64>
     {Md.CrEcb.decrypt_blocks(~T.LcTdesKey, ~L.LcBlock64, ~T.LcTdes.decrypt, k, Md.CrEcb.encrypt_blocks(~T.LcTdesKey, ~L.LcBlock64, ~T.LcTdes.encrypt, k, bs)) == bs : List<&2, L.LcBlock64>}
  LAWS.tdes_cbc_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=tdes_cbc_round_trip)
   # Triple DES (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
   law tdes_cbc_round_trip:
     for +k: T.LcTdesKey
     for +iv: L.LcBlock64
     for +bs: List<&2, L.LcBlock64>
     {Md.CrCbc.decrypt_blocks(~T.LcTdesKey, ~L.LcBlock64, ~T.LcTdes.decrypt, ~LC.CrBlk64.xor, k, iv, Md.CrCbc.encrypt_blocks(~T.LcTdesKey, ~L.LcBlock64, ~T.LcTdes.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
  LAWS.tdes_pcbc_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=tdes_pcbc_round_trip)
   # Triple DES (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
   law tdes_pcbc_round_trip:
     for +k: T.LcTdesKey
     for +iv: L.LcBlock64
     for +bs: List<&2, L.LcBlock64>
     {Pc.CrPcbc.decrypt_blocks(~T.LcTdesKey, ~L.LcBlock64, ~T.LcTdes.decrypt, ~LC.CrBlk64.xor, k, iv, Pc.CrPcbc.encrypt_blocks(~T.LcTdesKey, ~L.LcBlock64, ~T.LcTdes.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
  LAWS.sm4_block_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sm4_block_round_trip)
   # SM4 (legacy-ciphers): decryption undoes encryption, for every key and block
   law sm4_block_round_trip:
     for k: S.LcSm4Key
     for +b: M.CmBlock
     {S.LcSm4.decrypt(k, S.LcSm4.encrypt(k, b)) == b : M.CmBlock}
  LAWS.sm4_block_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sm4_block_round_trip_dual)
   # SM4 (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
   law sm4_block_round_trip_dual:
     for k: S.LcSm4Key
     for +b: M.CmBlock
     {S.LcSm4.encrypt(k, S.LcSm4.decrypt(k, b)) == b : M.CmBlock}
  LAWS.sm4_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sm4_key_length)
   # SM4 (legacy-ciphers): a key of 15 bytes is refused
   law sm4_key_length:
     {Result.map(&2, &2, Cr.CrError, S.LcSm4Key, Unit, k => Unit{}, LC.CrLc.key(~S.LcSm4Key, ~S.LcSm4.key, B.Octets.zeros(15n))) == Fail{Cr.CrBadKeyLength{15n}} : Result<&2, &2, Cr.CrError, Unit>}
  LAWS.sm4_ecb_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sm4_ecb_round_trip)
   # SM4 (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
   law sm4_ecb_round_trip:
     for +k: S.LcSm4Key
     for +bs: List<&2, M.CmBlock>
     {Md.CrEcb.decrypt_blocks(~S.LcSm4Key, ~M.CmBlock, ~S.LcSm4.decrypt, k, Md.CrEcb.encrypt_blocks(~S.LcSm4Key, ~M.CmBlock, ~S.LcSm4.encrypt, k, bs)) == bs : List<&2, M.CmBlock>}
  LAWS.sm4_cbc_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sm4_cbc_round_trip)
   # SM4 (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
   law sm4_cbc_round_trip:
     for +k: S.LcSm4Key
     for +iv: M.CmBlock
     for +bs: List<&2, M.CmBlock>
     {Md.CrCbc.decrypt_blocks(~S.LcSm4Key, ~M.CmBlock, ~S.LcSm4.decrypt, ~CM.CrBlk128.xor, k, iv, Md.CrCbc.encrypt_blocks(~S.LcSm4Key, ~M.CmBlock, ~S.LcSm4.encrypt, ~CM.CrBlk128.xor, k, iv, bs)) == bs : List<&2, M.CmBlock>}
  LAWS.sm4_pcbc_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sm4_pcbc_round_trip)
   # SM4 (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
   law sm4_pcbc_round_trip:
     for +k: S.LcSm4Key
     for +iv: M.CmBlock
     for +bs: List<&2, M.CmBlock>
     {Pc.CrPcbc.decrypt_blocks(~S.LcSm4Key, ~M.CmBlock, ~S.LcSm4.decrypt, ~CM.CrBlk128.xor, k, iv, Pc.CrPcbc.encrypt_blocks(~S.LcSm4Key, ~M.CmBlock, ~S.LcSm4.encrypt, ~CM.CrBlk128.xor, k, iv, bs)) == bs : List<&2, M.CmBlock>}
  LAWS.sm4_lrw_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=sm4_lrw_round_trip)
   # SM4 (legacy-ciphers) in LRW (lrw.bend): decryption undoes encryption, for every key, tweak key, index and list of blocks
   law sm4_lrw_round_trip:
     for +k: S.LcSm4Key
     for +k2: G.Gf128
     for +i: G.Gf128
     for +bs: List<&2, M.CmBlock>
     {Lw.CrLrw.decrypt_blocks(~S.LcSm4Key, ~M.CmBlock, ~S.LcSm4.decrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, k, k2, i, Lw.CrLrw.encrypt_blocks(~S.LcSm4Key, ~M.CmBlock, ~S.LcSm4.encrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, k, k2, i, bs)) == bs : List<&2, M.CmBlock>}
  LAWS.camellia_block_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=camellia_block_round_trip)
   # Camellia (legacy-ciphers): decryption undoes encryption, for every key and block
   law camellia_block_round_trip:
     for k: Ca.LcCamelliaKey
     for +b: M.CmBlock
     {Ca.LcCamellia.decrypt(k, Ca.LcCamellia.encrypt(k, b)) == b : M.CmBlock}
  LAWS.camellia_block_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=camellia_block_round_trip_dual)
   # Camellia (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
   law camellia_block_round_trip_dual:
     for k: Ca.LcCamelliaKey
     for +b: M.CmBlock
     {Ca.LcCamellia.encrypt(k, Ca.LcCamellia.decrypt(k, b)) == b : M.CmBlock}
  LAWS.camellia_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=camellia_key_length)
   # Camellia (legacy-ciphers): a key of 20 bytes is refused
   law camellia_key_length:
     {Result.map(&2, &2, Cr.CrError, Ca.LcCamelliaKey, Unit, k => Unit{}, LC.CrLc.key(~Ca.LcCamelliaKey, ~Ca.LcCamellia.key, B.Octets.zeros(20n))) == Fail{Cr.CrBadKeyLength{20n}} : Result<&2, &2, Cr.CrError, Unit>}
  LAWS.camellia_ecb_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=camellia_ecb_round_trip)
   # Camellia (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
   law camellia_ecb_round_trip:
     for +k: Ca.LcCamelliaKey
     for +bs: List<&2, M.CmBlock>
     {Md.CrEcb.decrypt_blocks(~Ca.LcCamelliaKey, ~M.CmBlock, ~Ca.LcCamellia.decrypt, k, Md.CrEcb.encrypt_blocks(~Ca.LcCamelliaKey, ~M.CmBlock, ~Ca.LcCamellia.encrypt, k, bs)) == bs : List<&2, M.CmBlock>}
  LAWS.camellia_cbc_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=camellia_cbc_round_trip)
   # Camellia (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
   law camellia_cbc_round_trip:
     for +k: Ca.LcCamelliaKey
     for +iv: M.CmBlock
     for +bs: List<&2, M.CmBlock>
     {Md.CrCbc.decrypt_blocks(~Ca.LcCamelliaKey, ~M.CmBlock, ~Ca.LcCamellia.decrypt, ~CM.CrBlk128.xor, k, iv, Md.CrCbc.encrypt_blocks(~Ca.LcCamelliaKey, ~M.CmBlock, ~Ca.LcCamellia.encrypt, ~CM.CrBlk128.xor, k, iv, bs)) == bs : List<&2, M.CmBlock>}
  LAWS.camellia_pcbc_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=camellia_pcbc_round_trip)
   # Camellia (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
   law camellia_pcbc_round_trip:
     for +k: Ca.LcCamelliaKey
     for +iv: M.CmBlock
     for +bs: List<&2, M.CmBlock>
     {Pc.CrPcbc.decrypt_blocks(~Ca.LcCamelliaKey, ~M.CmBlock, ~Ca.LcCamellia.decrypt, ~CM.CrBlk128.xor, k, iv, Pc.CrPcbc.encrypt_blocks(~Ca.LcCamelliaKey, ~M.CmBlock, ~Ca.LcCamellia.encrypt, ~CM.CrBlk128.xor, k, iv, bs)) == bs : List<&2, M.CmBlock>}
  LAWS.camellia_lrw_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=camellia_lrw_round_trip)
   # Camellia (legacy-ciphers) in LRW (lrw.bend): decryption undoes encryption, for every key, tweak key, index and list of blocks
   law camellia_lrw_round_trip:
     for +k: Ca.LcCamelliaKey
     for +k2: G.Gf128
     for +i: G.Gf128
     for +bs: List<&2, M.CmBlock>
     {Lw.CrLrw.decrypt_blocks(~Ca.LcCamelliaKey, ~M.CmBlock, ~Ca.LcCamellia.decrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, k, k2, i, Lw.CrLrw.encrypt_blocks(~Ca.LcCamelliaKey, ~M.CmBlock, ~Ca.LcCamellia.encrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, k, k2, i, bs)) == bs : List<&2, M.CmBlock>}
  LAWS.serpent_block_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=serpent_block_round_trip)
   # Serpent (legacy-ciphers): decryption undoes encryption, for every key and block
   law serpent_block_round_trip:
     for k: Sp.LcSerpentKey
     for +b: M.CmBlock
     {Sp.LcSerpent.decrypt(k, Sp.LcSerpent.encrypt(k, b)) == b : M.CmBlock}
  LAWS.serpent_block_round_trip_dual (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=serpent_block_round_trip_dual)
   # Serpent (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
   law serpent_block_round_trip_dual:
     for k: Sp.LcSerpentKey
     for +b: M.CmBlock
     {Sp.LcSerpent.encrypt(k, Sp.LcSerpent.decrypt(k, b)) == b : M.CmBlock}
  LAWS.serpent_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=serpent_key_length)
   # Serpent (legacy-ciphers): a key of 33 bytes is refused
   law serpent_key_length:
     {Result.map(&2, &2, Cr.CrError, Sp.LcSerpentKey, Unit, k => Unit{}, LC.CrLc.key(~Sp.LcSerpentKey, ~Sp.LcSerpent.key, B.Octets.zeros(33n))) == Fail{Cr.CrBadKeyLength{33n}} : Result<&2, &2, Cr.CrError, Unit>}
  LAWS.serpent_ecb_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&name=serpent_ecb_round_trip)
   # Serpent (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
   law serpent_ecb_round_trip:
     for +k: Sp.LcSerpentKey
     for +bs: List<&2, M.CmBlock>
     {Md.CrEcb.decrypt_blocks(~Sp.LcSerpentKey, ~M.CmBlock, ~Sp.LcSerpent.decrypt, k, Md.CrEcb.encrypt_blocks(~Sp.LcSerpentKey, ~M.CmBlock, ~Sp.LcSerpent.encrypt, k, bs)) == bs : List<&2, M.CmBlock>}
More: https://jend.leeeet.dev/packages/bend-osdev-crypto.txt?definitions_offset=100