LAWS.bend

bend-osdev-crypto@0.1.0.0 · 1,502 lines · 208 definitions

1# Laws of the interfaces and of the generic algorithms built on them.
2#
3# Generic laws (first part) hold for every algorithm that has an interface's
4# shape, so they are stated once over its template arguments: they need
5# nothing from the algorithm but its type. A law that needs a property of the
6# algorithm (a block cipher's decryption undoes its encryption, a hash in
7# pieces is the hash of the whole) cannot take that property as a hypothesis
8# and still pass --verdict (a template hypothesis has no model in the BendTT
9# kernel, and an ordinary one is affine, so an induction cannot use it at
10# every step). Those laws are stated once per instance instead, from the law
11# schemas in gen/instances.py, which also writes their proofs (second part).
12import Base
13import bend-osdev-bytes@0.1.0.0/bytes.bend as B
14import bend-osdev-word64@0.1.0.0/word64.bend as W
15import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
16import bend-osdev-cipher-modes@0.1.0.0/aes.bend as X
17import bend-osdev-cipher-modes@0.1.0.0/ccm.bend as MC
18import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
19import bend-osdev-legacy-ciphers@0.1.0.0/des.bend as D
20import bend-osdev-legacy-ciphers@0.1.0.0/tdes.bend as T
21import bend-osdev-legacy-ciphers@0.1.0.0/sm4.bend as S
22import bend-osdev-legacy-ciphers@0.1.0.0/camellia.bend as Ca
23import bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend as Sp
24import bend-osdev-legacy-ciphers@0.1.0.0/twofish.bend as Tf
25import bend-osdev-legacy-ciphers@0.1.0.0/rc4.bend as R
26import bend-osdev-legacy-ciphers@0.1.0.0/aria.bend as Ar
27import bend-osdev-legacy-ciphers@0.1.0.0/cast6.bend as C6
28import bend-osdev-legacy-ciphers@0.1.0.0/blowfish.bend as Bf
29import bend-osdev-legacy-ciphers@0.1.0.0/cast5.bend as C5
30import bend-osdev-legacy-ciphers@0.1.0.0/tea.bend as Te
31import bend-osdev-legacy-ciphers@0.1.0.0/xtea.bend as Xt
32import bend-osdev-legacy-ciphers@0.1.0.0/fcrypt.bend as Fc
33import bend-osdev-crc@0.1.0.0/crc.bend as C
34import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
35import bend-osdev-crypto@0.1.0.0/stream.bend as St
36import bend-osdev-crypto@0.1.0.0/block.bend as Bk
37import bend-osdev-crypto@0.1.0.0/modes.bend as Md
38import bend-osdev-crypto@0.1.0.0/pcbc.bend as Pc
39import bend-osdev-crypto@0.1.0.0/lrw.bend as Lw
40import bend-osdev-crypto@0.1.0.0/xcbc.bend as Xc
41import bend-osdev-crypto@0.1.0.0/vmac.bend as Vm
42import bend-osdev-crypto@0.1.0.0/cts.bend as Ct
43import bend-osdev-crypto@0.1.0.0/octets.bend as Oc
44import bend-osdev-gf@0.1.0.0/gf128.bend as G
45import bend-osdev-crypto@0.1.0.0/hash.bend as H
46import bend-osdev-crypto@0.1.0.0/mac.bend as Mc
47import bend-osdev-crypto@0.1.0.0/hmac.bend as Hm
48import bend-osdev-crypto@0.1.0.0/hkdf.bend as Hk
49import bend-osdev-crypto@0.1.0.0/sign.bend as Sg
50import bend-osdev-crypto@0.1.0.0/kex.bend as Kx
51import bend-osdev-crypto@0.1.0.0/inst_cm.bend as CM
52import bend-osdev-crypto@0.1.0.0/inst_lc.bend as LC
53import bend-osdev-crypto@0.1.0.0/inst_aes.bend as A
54import bend-osdev-crypto@0.1.0.0/inst_rc4.bend as RC
55import bend-osdev-crypto@0.1.0.0/inst_ccm.bend as CC
56import bend-osdev-crypto@0.1.0.0/inst_cmac.bend as CMI
57import bend-osdev-crypto@0.1.0.0/inst_crc.bend as CR
58import bend-osdev-crypto@0.1.0.0/inst_sha2.bend as SH
59import bend-osdev-crypto@0.1.0.0/inst_sha3.bend as S3
60import bend-osdev-hashes@0.1.0.0/hashes.bend as Hs
61import bend-osdev-hashes@0.1.0.0/md4.bend as HM4
62import bend-osdev-hashes@0.1.0.0/md5.bend as HM5
63import bend-osdev-hashes@0.1.0.0/sha1.bend as HS1
64import bend-osdev-hashes@0.1.0.0/ripemd160.bend as HRM
65import bend-osdev-hashes@0.1.0.0/sm3.bend as HSM
66import bend-osdev-hashes@0.1.0.0/streebog.bend as HST
67import bend-osdev-hashes@0.1.0.0/michael.bend as HMI
68import bend-osdev-crypto@0.1.0.0/inst_michael.bend as MIC
69import bend-osdev-crypto@0.1.0.0/pbkdf2.bend as Pb
70import bend-osdev-crypto@0.1.0.0/inst_pbkdf2.bend as PbI
71import bend-osdev-crypto@0.1.0.0/kbkdf.bend as Kb
72import bend-osdev-crypto@0.1.0.0/inst_kbkdf.bend as KbI
73import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha.bend as F256
74import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as F512
75import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend as F202
76
77# Stream ciphers from keystream generators (stream.bend): for every keystream
78# generator, CrXor satisfies the stream-cipher laws
79
80# the cipher is its own inverse: from one state, applied twice, the data
81# comes back
82law xor_involution:
83  for ~S: Data
84  for ~next: S -> St.CrKsStep<S>
85  for +s: S
86  for +m: B.Octets
87  {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}
88
89# data in pieces: the output of a ++ b is the output of a, then the output of
90# b from the state after a
91law xor_streaming_data:
92  for ~S: Data
93  for ~next: S -> St.CrKsStep<S>
94  for +s: S
95  for +a: B.Octets
96  for +b: B.Octets
97  {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}
98
99law xor_streaming_state:
100  for ~S: Data
101  for ~next: S -> St.CrKsStep<S>
102  for +s: S
103  for +a: B.Octets
104  for +b: B.Octets
105  {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}
106
107# CTR over any block cipher (modes.bend) is CrXor over its keystream
108# generator, so it satisfies the stream-cipher laws for every block cipher
109
110law ctr_involution:
111  for ~K: Data
112  for ~Blk: Data
113  for ~enc: K -> Blk -> Blk
114  for ~blk_of: B.Octets -> Maybe<&2, Blk>
115  for ~blk_to: Blk -> B.Octets
116  for +s: Md.CrCtrState<K>
117  for +m: B.Octets
118  {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}
119
120law ctr_streaming_data:
121  for ~K: Data
122  for ~Blk: Data
123  for ~enc: K -> Blk -> Blk
124  for ~blk_of: B.Octets -> Maybe<&2, Blk>
125  for ~blk_to: Blk -> B.Octets
126  for +s: Md.CrCtrState<K>
127  for +a: B.Octets
128  for +b: B.Octets
129  {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}
130
131law ctr_streaming_state:
132  for ~K: Data
133  for ~Blk: Data
134  for ~enc: K -> Blk -> Blk
135  for ~blk_of: B.Octets -> Maybe<&2, Blk>
136  for ~blk_to: Blk -> B.Octets
137  for +s: Md.CrCtrState<K>
138  for +a: B.Octets
139  for +b: B.Octets
140  {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>}
141
142# The block formats (inst_cm.bend, inst_lc.bend): a block read back from its
143# bytes is itself, and XOR with the same block twice changes nothing
144
145law cmblock_format:
146  for +b: M.CmBlock
147  {CM.CrBlk128.of_octets(CM.CrBlk128.to_octets(b)) == Some{b} : Maybe<&2, M.CmBlock>}
148
149law cmblock_xor:
150  for a: M.CmBlock
151  for b: M.CmBlock
152  {CM.CrBlk128.xor(CM.CrBlk128.xor(a, b), b) == a : M.CmBlock}
153
154law lcblock64_format:
155  for +b: L.LcBlock64
156  {L.LcBlock64.of_octets(L.LcBlock64.to_octets(b)) == Some{b} : Maybe<&2, L.LcBlock64>}
157
158law lcblock64_xor:
159  for a: L.LcBlock64
160  for b: L.LcBlock64
161  {LC.CrBlk64.xor(LC.CrBlk64.xor(a, b), b) == a : L.LcBlock64}
162
163# MACs (mac.bend): the named default verify accepts the computed tag, and
164# exactly it, for every MAC; so HMAC over any hash, and CMAC over any 128-bit
165# block cipher, accept what they compute
166
167law mac_verify_tag_accepts:
168  for ~K: Data
169  for ~compute: K -> B.Octets -> B.Octets
170  for +k: K
171  for +m: B.Octets
172  {Mc.CrMac.verify_tag(~K, ~compute, k, m, compute(k, m)) == True{} : Bool}
173
174law mac_verify_tag_agrees:
175  for ~K: Data
176  for ~compute: K -> B.Octets -> B.Octets
177  for +k: K
178  for +m: B.Octets
179  for t: B.Octets
180  {Mc.CrMac.verify_tag(~K, ~compute, k, m, t) == B.Octets.is_eq(compute(k, m), t) : Bool}
181
182law hmac_accepts:
183  for ~digest: B.Octets -> B.Octets
184  for +kk: Hm.CrHmacKey
185  for +m: B.Octets
186  {Hm.CrHmac.verify(~digest, kk, m, Hm.CrHmac.mac(~digest, kk, m)) == True{} : Bool}
187
188law cmac_accepts:
189  for ~K: Data
190  for ~enc: K -> M.CmBlock -> M.CmBlock
191  for +k: K
192  for +m: B.Octets
193  {CMI.CrCmac.verify(~K, ~enc, k, m, CMI.CrCmac.mac(~K, ~enc, k, m)) == True{} : Bool}
194
195# XCBC-MAC over every block cipher (xcbc.bend) accepts what it computes
196law xcbc_accepts:
197  for ~K: Data
198  for ~Blk: Data
199  for ~bsize: Nat
200  for ~enc: K -> Blk -> Blk
201  for ~blk_of: B.Octets -> Maybe<&2, Blk>
202  for ~blk_to: Blk -> B.Octets
203  for +kk: Xc.CrXcbcKey<K>
204  for +m: B.Octets
205  {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}
206
207# VMAC over every block cipher and nonce length (vmac.bend) accepts what it
208# computes
209law vmac_accepts:
210  for ~K: Data
211  for ~Blk: Data
212  for ~bsize: Nat
213  for ~enc: K -> Blk -> Blk
214  for ~blk_of: B.Octets -> Maybe<&2, Blk>
215  for ~blk_to: Blk -> B.Octets
216  for ~nlen: Nat
217  for +kk: Vm.CrVmacKey<K>
218  for +m: B.Octets
219  {Vm.CrVmac.verify(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, ~nlen, kk, m, Vm.CrVmac.mac(~K, ~Blk, ~bsize, ~enc, ~blk_of, ~blk_to, ~nlen, kk, m)) == True{} : Bool}
220
221# CRCs as hashes (inst_crc.bend), for every parameter set: the register in
222# pieces is the register of the whole, and so the streaming digest of any
223# split is the one-shot digest
224
225law crc32_hash_streaming:
226  for ~spec: C.Crc32Spec
227  for c: U32
228  for +a: B.Octets
229  for +b: B.Octets
230  {CR.CrCrc32.update(~spec, c, B.Octets.append(a, b)) == CR.CrCrc32.update(~spec, CR.CrCrc32.update(~spec, c, a), b) : U32}
231
232law crc32_hash_split:
233  for ~spec: C.Crc32Spec
234  for +a: B.Octets
235  for +b: B.Octets
236  {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}
237
238law crc64_hash_streaming:
239  for ~spec: C.Crc64Spec
240  for c: W.W64
241  for +a: B.Octets
242  for +b: B.Octets
243  {CR.CrCrc64.update(~spec, c, B.Octets.append(a, b)) == CR.CrCrc64.update(~spec, CR.CrCrc64.update(~spec, c, a), b) : W.W64}
244
245law crc64_hash_split:
246  for ~spec: C.Crc64Spec
247  for +a: B.Octets
248  for +b: B.Octets
249  {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}
250
251# AEADs: an algorithm's round trip survives the mapping of its errors onto
252# CrError, for every algorithm (r: its encryption's result, d: its
253# decryption)
254
255law lift_round_trip:
256  for ~E: Data
257  for ~f: E -> Cr.CrError
258  for d: B.Octets -> Result<&2, &2, E, B.Octets>
259  for r: Result<&2, &2, E, B.Octets>
260  for +p: B.Octets
261  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>}
262  {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>}
263
264# CCM as an AEAD (inst_ccm.bend), for every 128-bit block cipher, key, tag
265# length, nonce, associated data and message: the AEAD round trip, given
266# cipher-modes' ccm_round_trip at the same arguments (h). cipher-modes
267# proves h for every input, but a proof that imports its PROOF.bend fails
268# --verdict (its laws with a template hypothesis), so the two are joined in
269# README.md, not here.
270law ccm_round_trip_if:
271  for ~K: Data
272  for ~enc: K -> M.CmBlock -> M.CmBlock
273  for ~tlen: Nat
274  for +k: K
275  for +nonce: B.Octets
276  for +aad: B.Octets
277  for +p: B.Octets
278  for h: {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, MC.Ccm.encrypt(~K, ~enc, k, tlen, nonce, aad, p), c => MC.Ccm.decrypt(~K, ~enc, k, tlen, nonce, aad, c)) == Result.map(&2, &2, M.CmError, B.Octets, B.Octets, c => p, MC.Ccm.encrypt(~K, ~enc, k, tlen, nonce, aad, p)) : Result<&2, &2, M.CmError, B.Octets>}
279  {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, CC.CrCcm.seal(~K, ~enc, ~tlen, k, nonce, aad, p), c => CC.CrCcm.open(~K, ~enc, ~tlen, k, nonce, aad, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, CC.CrCcm.seal(~K, ~enc, ~tlen, k, nonce, aad, p)) : Result<&2, &2, Cr.CrError, B.Octets>}
280
281# Signatures and key agreement (sign.bend, kex.bend): the generic helpers
282# keep the interface laws (README.md); the instances (RSA, DH, ECDSA, ECDH,
283# SM2, EC-RDSA) and their laws are in bend-osdev-pubkey. A signature
284# checked from the public key's bytes is accepted, for every scheme, secret
285# key and message, when the scheme's pk_format and accepts laws hold there
286# (hf, ha)
287law sign_verify_bytes_if:
288  for ~SK: Data
289  for ~PK: Data
290  for ~public: SK -> PK
291  for ~pk_of: B.Octets -> Result<&2, &2, Cr.CrError, PK>
292  for ~pk_to: PK -> B.Octets
293  for ~sign: SK -> B.Octets -> B.Octets
294  for ~verify: PK -> B.Octets -> B.Octets -> Bool
295  for +sk: SK
296  for +m: B.Octets
297  for hf: {pk_of(pk_to(public(sk))) == Done{public(sk)} : Result<&2, &2, Cr.CrError, PK>}
298  for ha: {verify(public(sk), m, sign(sk, m)) == True{} : Bool}
299  {Sg.CrSign.verify_bytes(~PK, ~pk_of, ~verify, pk_to(public(sk)), m, sign(sk, m)) == True{} : Bool}
300
301# two parties agree from each other's public-key bytes, for every scheme and
302# pair of secret keys, when the keys parse (hx, hy), the public keys survive
303# their bytes (hfx, hfy) and the scheme's agree law holds for them (h)
304law kex_agree_if:
305  for ~SK: Data
306  for ~PK: Data
307  for ~secret: B.Octets -> Result<&2, &2, Cr.CrError, SK>
308  for ~public: SK -> PK
309  for ~pk_of: B.Octets -> Result<&2, &2, Cr.CrError, PK>
310  for ~pk_to: PK -> B.Octets
311  for ~shared: SK -> PK -> Result<&2, &2, Cr.CrError, B.Octets>
312  for +a: B.Octets
313  for +b: B.Octets
314  for +x: SK
315  for +y: SK
316  for hx: {secret(a) == Done{x} : Result<&2, &2, Cr.CrError, SK>}
317  for hy: {secret(b) == Done{y} : Result<&2, &2, Cr.CrError, SK>}
318  for hfx: {pk_of(pk_to(public(x))) == Done{public(x)} : Result<&2, &2, Cr.CrError, PK>}
319  for hfy: {pk_of(pk_to(public(y))) == Done{public(y)} : Result<&2, &2, Cr.CrError, PK>}
320  for h: {shared(x, public(y)) == shared(y, public(x)) : Result<&2, &2, Cr.CrError, B.Octets>}
321  {Kx.CrKex.agree(~SK, ~PK, ~secret, ~pk_of, ~shared, a, pk_to(public(y))) == Kx.CrKex.agree(~SK, ~PK, ~secret, ~pk_of, ~shared, b, pk_to(public(x))) : Result<&2, &2, Cr.CrError, B.Octets>}
322
323# Vectors, proved by computation: CRC check values (the reveng catalogue)
324# through the hash interface
325
326law crc32_hash_check:
327  {CR.CrCrc32.digest(~C.crc32.spec(), B.Octets.of_string("123456789")) == B.Octets.of_list([203, 244, 57, 38]) : B.Octets}
328
329law crc32c_hash_check:
330  {CR.CrCrc32.digest(~C.crc32c.spec(), B.Octets.of_string("123456789")) == B.Octets.of_list([227, 6, 146, 131]) : B.Octets}
331
332law crc64_xz_hash_check:
333  {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}
334
335# a CRC-32 digest is 4 bytes, for every parameter set and register
336law crc32_hash_length:
337  for ~spec: C.Crc32Spec
338  for c: U32
339  {B.Octets.len(CR.CrCrc32.final(~spec, c)) == 4n : Nat}
340
341# HMAC over CRC-32 (the key "key", the message "The quick brown fox"): the
342# value of Python's hmac module over binascii.crc32 (ref/gen.py checks the
343# same construction on random keys and messages)
344law hmac_crc32_vector:
345  {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}
346
347# refusals: an RC4 key of 0 bytes, an IV given to RC4, a CTR counter block
348# of the wrong length, bytes that are not whole blocks, and an HKDF output
349# longer than 255 digests
350law rc4_empty_key:
351  {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>}
352
353law rc4_iv_refused:
354  {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>}
355
356law ctr_bad_iv:
357  {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>}
358
359law blocks_of_not_whole:
360  {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>}
361
362law hkdf_too_long:
363  {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>}
364
365# FIPS 197 Appendix C.1 through the block-cipher interface: AES-128, its
366# encryption key schedule then one block of bytes (with CrAes.key, which
367# computes the decryption round keys too, the vector checks but runs past
368# --verdict's kernel; check.bend runs it both ways)
369law aes_fips197_c1:
370  {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>}
371
372# A CRC in three pieces is the CRC of the whole, for every parameter set
373
374law crc32_hash_split3:
375  for ~spec: C.Crc32Spec
376  for +a: B.Octets
377  for +b: B.Octets
378  for +c: B.Octets
379  {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}
380
381law crc64_hash_split3:
382  for ~spec: C.Crc64Spec
383  for +a: B.Octets
384  for +b: B.Octets
385  for +c: B.Octets
386  {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}
387
388# SHA-256 and SHA-512 as hashes (inst_sha2.bend), from
389# bend-collections-laws-crypto's laws: the one-shot digest is FIPS 180-4's
390# executable specification (in that package's spec/), the streaming digest
391# of any split into two or three pieces is the one-shot digest, and a
392# digest is 32 (64) bytes. bend-collections proves the pieces only from the
393# start (new_sha256()), so the stronger streaming law (for every state) is
394# tested, not proved.
395
396law sha256_spec:
397  for +o: B.Octets
398  {SH.CrSha2.sha256(o) == B.Octets.of_list(F256.sha256_bytes(B.Octets.to_list(o))) : B.Octets}
399
400law sha256_hash_split:
401  for +a: B.Octets
402  for +b: B.Octets
403  {SH.CrSha2.final(SH.CrSha2.update(SH.CrSha2.update(SH.CrSha2.init256(), a), b)) == SH.CrSha2.sha256(B.Octets.append(a, b)) : B.Octets}
404
405law sha256_hash_split3:
406  for +a: B.Octets
407  for +b: B.Octets
408  for +c: B.Octets
409  {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}
410
411law sha256_hash_length:
412  for +o: B.Octets
413  {B.Octets.len(SH.CrSha2.sha256(o)) == 32n : Nat}
414
415law sha512_spec:
416  for +o: B.Octets
417  {SH.CrSha2.sha512(o) == B.Octets.of_list(F512.sha512_bytes(B.Octets.to_list(o))) : B.Octets}
418
419law sha512_hash_split:
420  for +a: B.Octets
421  for +b: B.Octets
422  {SH.CrSha2.final(SH.CrSha2.update(SH.CrSha2.update(SH.CrSha2.init512(), a), b)) == SH.CrSha2.sha512(B.Octets.append(a, b)) : B.Octets}
423
424law sha512_hash_split3:
425  for +a: B.Octets
426  for +b: B.Octets
427  for +c: B.Octets
428  {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}
429
430law sha512_hash_length:
431  for +o: B.Octets
432  {B.Octets.len(SH.CrSha2.sha512(o)) == 64n : Nat}
433
434# SHA3-256 as a hash (inst_sha3.bend), from bend-collections-laws-crypto's
435# laws, as for SHA-2: the one-shot digest is FIPS 202's executable
436# specification (that package's spec/crypto/sha3.bend), the streaming
437# digest of any split into two or three pieces is the one-shot digest, and
438# a digest is 32 bytes. As for SHA-2, the streaming law for every state is
439# tested, not proved.
440
441law sha3_256_spec:
442  for +o: B.Octets
443  {S3.CrSha3.sha3_256(o) == B.Octets.of_list(F202.sha3_256(B.Octets.to_list(o))) : B.Octets}
444
445law sha3_256_hash_split:
446  for +a: B.Octets
447  for +b: B.Octets
448  {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}
449
450law sha3_256_hash_split3:
451  for +a: B.Octets
452  for +b: B.Octets
453  for +c: B.Octets
454  {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}
455
456law sha3_256_hash_length:
457  for +o: B.Octets
458  {B.Octets.len(S3.CrSha3.sha3_256(o)) == 32n : Nat}
459
460# HKDF over SHA-256 refuses more than 255 digests (8160 bytes)
461law hkdf_sha256_too_long:
462  {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>}
463
464# FIPS 180-4's example "abc" (NIST's SHA examples), through the hash
465# interface
466law sha256_abc:
467  {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}
468
469# FIPS 202's SHA3-256 of "abc" (NIST's SHA-3 examples), through the hash
470# interface
471law sha3_256_abc:
472  {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}
473
474# RFC 4231 test case 2: HMAC-SHA-256 with the key "Jefe"
475law hmac_sha256_rfc4231_2:
476  {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}
477
478# Michael as a MAC (inst_michael.bend): it accepts what it computes, for
479# every key and message (it uses the named default verify); a key of
480# another length than 8 bytes is refused; the sixth test vector recalled as
481# IEEE 802.11i's, through the MAC interface (not checked against a published
482# copy: hashes/README.md)
483law michael_accepts:
484  for +k: Hs.HsW2
485  for +m: B.Octets
486  {MIC.CrMichael.verify(k, m, HMI.HsMichael.mic(k, m)) == True{} : Bool}
487
488law michael_key_length:
489  {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>}
490
491law michael_mac_vector:
492  {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>}
493
494# PBKDF2 over any MAC (pbkdf2.bend), for every MAC, password, salt,
495# iteration count and length: a derivation that succeeds gives exactly the
496# length asked for (the KDF interface's length law); the unchecked stream
497# has that length, and a shorter stream is a prefix of a longer (the KDF
498# interface's prefix law)
499law pbkdf2_length:
500  for ~K: Data
501  for ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>
502  for ~compute: K -> B.Octets -> B.Octets
503  for ~hlen: Nat
504  for +p: B.Octets
505  for +salt: B.Octets
506  for +c: U32
507  for +n: Nat
508  {Result.map(&2, &2, Cr.CrError, B.Octets, Nat, o => B.Octets.len(o), Pb.CrPbkdf2.pbkdf2(~K, ~key, ~compute, ~hlen, p, salt, c, n)) == Result.map(&2, &2, Cr.CrError, B.Octets, Nat, o => n, Pb.CrPbkdf2.pbkdf2(~K, ~key, ~compute, ~hlen, p, salt, c, n)) : Result<&2, &2, Cr.CrError, Nat>}
509
510law pbkdf2_stream_length:
511  for ~K: Data
512  for ~compute: K -> B.Octets -> B.Octets
513  for +k: K
514  for +salt: B.Octets
515  for +c: U32
516  for +n: Nat
517  {B.Octets.len(Pb.CrPbkdf2.stream(~K, ~compute, k, salt, c, n)) == n : Nat}
518
519law pbkdf2_stream_prefix:
520  for ~K: Data
521  for ~compute: K -> B.Octets -> B.Octets
522  for +k: K
523  for +salt: B.Octets
524  for +c: U32
525  for +n: Nat
526  for +j: Nat
527  {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}
528
529# PBKDF2 refuses an iteration count of 0 (over HMAC-SHA-1)
530law pbkdf2_zero_iterations:
531  {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>}
532
533# RFC 6070 test cases 1 and 2: PBKDF2-HMAC-SHA1, P = "password",
534# S = "salt", c = 1 and 2, dkLen = 20
535law pbkdf2_hmac_sha1_rfc6070_1:
536  {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>}
537
538law pbkdf2_hmac_sha1_rfc6070_2:
539  {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>}
540
541# RFC 7914, section 11: PBKDF2-HMAC-SHA256, P = "passwd", S = "salt",
542# c = 1: the first 32 of its 64 bytes (a shorter output is a prefix of a
543# longer, pbkdf2_stream_prefix; all 64 bytes, two blocks, run past
544# --verdict's kernel fuel, and check.bend computes them)
545law pbkdf2_hmac_sha256_rfc7914_1:
546  {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>}
547
548# SP 800-108 KDFs over any MAC (kbkdf.bend), for every MAC, key, fixed
549# input data and length: each stream has the length asked for, a shorter
550# stream is a prefix of a longer one with the same fixed input (and IV), and
551# a derivation that succeeds has the length asked for. (The interface's
552# prefix law holds of the streams: a derivation binds its length L into
553# the fixed input, so derivations of two lengths differ.)
554law kbkdf_counter_stream_length:
555  for ~K: Data
556  for ~compute: K -> B.Octets -> B.Octets
557  for ~rlen: Nat
558  for +k: K
559  for +fixed: B.Octets
560  for +n: Nat
561  {B.Octets.len(Kb.CrKbkdf.counter_stream(~K, ~compute, ~rlen, k, fixed, n)) == n : Nat}
562
563law kbkdf_counter_stream_prefix:
564  for ~K: Data
565  for ~compute: K -> B.Octets -> B.Octets
566  for ~rlen: Nat
567  for +k: K
568  for +fixed: B.Octets
569  for +n: Nat
570  for +j: Nat
571  {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}
572
573law kbkdf_feedback_stream_length:
574  for ~K: Data
575  for ~compute: K -> B.Octets -> B.Octets
576  for ~rlen: Nat
577  for +k: K
578  for +iv: B.Octets
579  for +fixed: B.Octets
580  for +n: Nat
581  {B.Octets.len(Kb.CrKbkdf.feedback_stream(~K, ~compute, ~rlen, k, iv, fixed, n)) == n : Nat}
582
583law kbkdf_feedback_stream_prefix:
584  for ~K: Data
585  for ~compute: K -> B.Octets -> B.Octets
586  for ~rlen: Nat
587  for +k: K
588  for +iv: B.Octets
589  for +fixed: B.Octets
590  for +n: Nat
591  for +j: Nat
592  {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}
593
594law kbkdf_counter_length:
595  for ~K: Data
596  for ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>
597  for ~compute: K -> B.Octets -> B.Octets
598  for ~hlen: Nat
599  for ~rlen: Nat
600  for ~llen: Nat
601  for +ki: B.Octets
602  for +label: B.Octets
603  for +context: B.Octets
604  for +n: Nat
605  {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>}
606
607law kbkdf_feedback_length:
608  for ~K: Data
609  for ~key: B.Octets -> Result<&2, &2, Cr.CrError, K>
610  for ~compute: K -> B.Octets -> B.Octets
611  for ~hlen: Nat
612  for ~rlen: Nat
613  for ~llen: Nat
614  for +ki: B.Octets
615  for +iv: B.Octets
616  for +label: B.Octets
617  for +context: B.Octets
618  for +n: Nat
619  {Result.map(&2, &2, Cr.CrError, B.Octets, Nat, o => B.Octets.len(o), Kb.CrKbkdf.feedback_kdf(~K, ~key, ~compute, ~hlen, ~rlen, ~llen, ki, iv, label, context, n)) == Result.map(&2, &2, Cr.CrError, B.Octets, Nat, o => n, Kb.CrKbkdf.feedback_kdf(~K, ~key, ~compute, ~hlen, ~rlen, ~llen, ki, iv, label, context, n)) : Result<&2, &2, Cr.CrError, Nat>}
620
621# KBKDF in counter mode over HMAC-SHA-256 (32-bit counter and [L]_2), the
622# key "secret key bytes", Label "label", Context "context", 32 bytes:
623# Python's cryptography's KBKDFHMAC gives this value. Stated on the stream
624# (what CrKbkdf.counter_kdf returns once its length checks pass): those
625# checks compare with 2^32, which --verdict's kernel cannot compute in time;
626# check.bend runs the checked derivation
627law kbkdf_hmac_sha256_vector:
628  {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}
629
630# Per-instance laws, from the law schemas (gen/instances.py)
631
632# BEGIN GENERATED by gen/instances.py: laws
633# DES (legacy-ciphers): decryption undoes encryption, for every key and block
634law des_block_round_trip:
635  for k: D.LcDesKey
636  for +b: L.LcBlock64
637  {D.LcDes.decrypt(k, D.LcDes.encrypt(k, b)) == b : L.LcBlock64}
638
639# DES (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
640law des_block_round_trip_dual:
641  for k: D.LcDesKey
642  for +b: L.LcBlock64
643  {D.LcDes.encrypt(k, D.LcDes.decrypt(k, b)) == b : L.LcBlock64}
644
645# DES (legacy-ciphers): a key of 7 bytes is refused
646law des_key_length:
647  {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>}
648
649# DES (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
650law des_ecb_round_trip:
651  for +k: D.LcDesKey
652  for +bs: List<&2, L.LcBlock64>
653  {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>}
654
655# DES (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
656law des_cbc_round_trip:
657  for +k: D.LcDesKey
658  for +iv: L.LcBlock64
659  for +bs: List<&2, L.LcBlock64>
660  {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>}
661
662# DES (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
663law des_pcbc_round_trip:
664  for +k: D.LcDesKey
665  for +iv: L.LcBlock64
666  for +bs: List<&2, L.LcBlock64>
667  {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>}
668
669# Triple DES (legacy-ciphers): decryption undoes encryption, for every key and block
670law tdes_block_round_trip:
671  for k: T.LcTdesKey
672  for +b: L.LcBlock64
673  {T.LcTdes.decrypt(k, T.LcTdes.encrypt(k, b)) == b : L.LcBlock64}
674
675# Triple DES (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
676law tdes_block_round_trip_dual:
677  for k: T.LcTdesKey
678  for +b: L.LcBlock64
679  {T.LcTdes.encrypt(k, T.LcTdes.decrypt(k, b)) == b : L.LcBlock64}
680
681# Triple DES (legacy-ciphers): a key of 8 bytes is refused
682law tdes_key_length:
683  {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>}
684
685# Triple DES (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
686law tdes_ecb_round_trip:
687  for +k: T.LcTdesKey
688  for +bs: List<&2, L.LcBlock64>
689  {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>}
690
691# Triple DES (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
692law tdes_cbc_round_trip:
693  for +k: T.LcTdesKey
694  for +iv: L.LcBlock64
695  for +bs: List<&2, L.LcBlock64>
696  {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>}
697
698# Triple DES (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
699law tdes_pcbc_round_trip:
700  for +k: T.LcTdesKey
701  for +iv: L.LcBlock64
702  for +bs: List<&2, L.LcBlock64>
703  {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>}
704
705# SM4 (legacy-ciphers): decryption undoes encryption, for every key and block
706law sm4_block_round_trip:
707  for k: S.LcSm4Key
708  for +b: M.CmBlock
709  {S.LcSm4.decrypt(k, S.LcSm4.encrypt(k, b)) == b : M.CmBlock}
710
711# SM4 (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
712law sm4_block_round_trip_dual:
713  for k: S.LcSm4Key
714  for +b: M.CmBlock
715  {S.LcSm4.encrypt(k, S.LcSm4.decrypt(k, b)) == b : M.CmBlock}
716
717# SM4 (legacy-ciphers): a key of 15 bytes is refused
718law sm4_key_length:
719  {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>}
720
721# SM4 (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
722law sm4_ecb_round_trip:
723  for +k: S.LcSm4Key
724  for +bs: List<&2, M.CmBlock>
725  {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>}
726
727# SM4 (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
728law sm4_cbc_round_trip:
729  for +k: S.LcSm4Key
730  for +iv: M.CmBlock
731  for +bs: List<&2, M.CmBlock>
732  {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>}
733
734# SM4 (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
735law sm4_pcbc_round_trip:
736  for +k: S.LcSm4Key
737  for +iv: M.CmBlock
738  for +bs: List<&2, M.CmBlock>
739  {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>}
740
741# SM4 (legacy-ciphers) in LRW (lrw.bend): decryption undoes encryption, for every key, tweak key, index and list of blocks
742law sm4_lrw_round_trip:
743  for +k: S.LcSm4Key
744  for +k2: G.Gf128
745  for +i: G.Gf128
746  for +bs: List<&2, M.CmBlock>
747  {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>}
748
749# Camellia (legacy-ciphers): decryption undoes encryption, for every key and block
750law camellia_block_round_trip:
751  for k: Ca.LcCamelliaKey
752  for +b: M.CmBlock
753  {Ca.LcCamellia.decrypt(k, Ca.LcCamellia.encrypt(k, b)) == b : M.CmBlock}
754
755# Camellia (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
756law camellia_block_round_trip_dual:
757  for k: Ca.LcCamelliaKey
758  for +b: M.CmBlock
759  {Ca.LcCamellia.encrypt(k, Ca.LcCamellia.decrypt(k, b)) == b : M.CmBlock}
760
761# Camellia (legacy-ciphers): a key of 20 bytes is refused
762law camellia_key_length:
763  {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>}
764
765# Camellia (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
766law camellia_ecb_round_trip:
767  for +k: Ca.LcCamelliaKey
768  for +bs: List<&2, M.CmBlock>
769  {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>}
770
771# Camellia (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
772law camellia_cbc_round_trip:
773  for +k: Ca.LcCamelliaKey
774  for +iv: M.CmBlock
775  for +bs: List<&2, M.CmBlock>
776  {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>}
777
778# Camellia (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
779law camellia_pcbc_round_trip:
780  for +k: Ca.LcCamelliaKey
781  for +iv: M.CmBlock
782  for +bs: List<&2, M.CmBlock>
783  {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>}
784
785# Camellia (legacy-ciphers) in LRW (lrw.bend): decryption undoes encryption, for every key, tweak key, index and list of blocks
786law camellia_lrw_round_trip:
787  for +k: Ca.LcCamelliaKey
788  for +k2: G.Gf128
789  for +i: G.Gf128
790  for +bs: List<&2, M.CmBlock>
791  {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>}
792
793# Serpent (legacy-ciphers): decryption undoes encryption, for every key and block
794law serpent_block_round_trip:
795  for k: Sp.LcSerpentKey
796  for +b: M.CmBlock
797  {Sp.LcSerpent.decrypt(k, Sp.LcSerpent.encrypt(k, b)) == b : M.CmBlock}
798
799# Serpent (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
800law serpent_block_round_trip_dual:
801  for k: Sp.LcSerpentKey
802  for +b: M.CmBlock
803  {Sp.LcSerpent.encrypt(k, Sp.LcSerpent.decrypt(k, b)) == b : M.CmBlock}
804
805# Serpent (legacy-ciphers): a key of 33 bytes is refused
806law serpent_key_length:
807  {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>}
808
809# Serpent (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
810law serpent_ecb_round_trip:
811  for +k: Sp.LcSerpentKey
812  for +bs: List<&2, M.CmBlock>
813  {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>}
814
815# Serpent (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
816law serpent_cbc_round_trip:
817  for +k: Sp.LcSerpentKey
818  for +iv: M.CmBlock
819  for +bs: List<&2, M.CmBlock>
820  {Md.CrCbc.decrypt_blocks(~Sp.LcSerpentKey, ~M.CmBlock, ~Sp.LcSerpent.decrypt, ~CM.CrBlk128.xor, k, iv, Md.CrCbc.encrypt_blocks(~Sp.LcSerpentKey, ~M.CmBlock, ~Sp.LcSerpent.encrypt, ~CM.CrBlk128.xor, k, iv, bs)) == bs : List<&2, M.CmBlock>}
821
822# Serpent (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
823law serpent_pcbc_round_trip:
824  for +k: Sp.LcSerpentKey
825  for +iv: M.CmBlock
826  for +bs: List<&2, M.CmBlock>
827  {Pc.CrPcbc.decrypt_blocks(~Sp.LcSerpentKey, ~M.CmBlock, ~Sp.LcSerpent.decrypt, ~CM.CrBlk128.xor, k, iv, Pc.CrPcbc.encrypt_blocks(~Sp.LcSerpentKey, ~M.CmBlock, ~Sp.LcSerpent.encrypt, ~CM.CrBlk128.xor, k, iv, bs)) == bs : List<&2, M.CmBlock>}
828
829# Serpent (legacy-ciphers) in LRW (lrw.bend): decryption undoes encryption, for every key, tweak key, index and list of blocks
830law serpent_lrw_round_trip:
831  for +k: Sp.LcSerpentKey
832  for +k2: G.Gf128
833  for +i: G.Gf128
834  for +bs: List<&2, M.CmBlock>
835  {Lw.CrLrw.decrypt_blocks(~Sp.LcSerpentKey, ~M.CmBlock, ~Sp.LcSerpent.decrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, k, k2, i, Lw.CrLrw.encrypt_blocks(~Sp.LcSerpentKey, ~M.CmBlock, ~Sp.LcSerpent.encrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, k, k2, i, bs)) == bs : List<&2, M.CmBlock>}
836
837# Twofish (legacy-ciphers): decryption undoes encryption, for every key and block
838law twofish_block_round_trip:
839  for k: Tf.LcTwofishKey
840  for +b: M.CmBlock
841  {Tf.LcTwofish.decrypt(k, Tf.LcTwofish.encrypt(k, b)) == b : M.CmBlock}
842
843# Twofish (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
844law twofish_block_round_trip_dual:
845  for k: Tf.LcTwofishKey
846  for +b: M.CmBlock
847  {Tf.LcTwofish.encrypt(k, Tf.LcTwofish.decrypt(k, b)) == b : M.CmBlock}
848
849# Twofish (legacy-ciphers): a key of 20 bytes is refused
850law twofish_key_length:
851  {Result.map(&2, &2, Cr.CrError, Tf.LcTwofishKey, Unit, k => Unit{}, LC.CrLc.key(~Tf.LcTwofishKey, ~Tf.LcTwofish.key, B.Octets.zeros(20n))) == Fail{Cr.CrBadKeyLength{20n}} : Result<&2, &2, Cr.CrError, Unit>}
852
853# Twofish (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
854law twofish_ecb_round_trip:
855  for +k: Tf.LcTwofishKey
856  for +bs: List<&2, M.CmBlock>
857  {Md.CrEcb.decrypt_blocks(~Tf.LcTwofishKey, ~M.CmBlock, ~Tf.LcTwofish.decrypt, k, Md.CrEcb.encrypt_blocks(~Tf.LcTwofishKey, ~M.CmBlock, ~Tf.LcTwofish.encrypt, k, bs)) == bs : List<&2, M.CmBlock>}
858
859# Twofish (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
860law twofish_cbc_round_trip:
861  for +k: Tf.LcTwofishKey
862  for +iv: M.CmBlock
863  for +bs: List<&2, M.CmBlock>
864  {Md.CrCbc.decrypt_blocks(~Tf.LcTwofishKey, ~M.CmBlock, ~Tf.LcTwofish.decrypt, ~CM.CrBlk128.xor, k, iv, Md.CrCbc.encrypt_blocks(~Tf.LcTwofishKey, ~M.CmBlock, ~Tf.LcTwofish.encrypt, ~CM.CrBlk128.xor, k, iv, bs)) == bs : List<&2, M.CmBlock>}
865
866# Twofish (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
867law twofish_pcbc_round_trip:
868  for +k: Tf.LcTwofishKey
869  for +iv: M.CmBlock
870  for +bs: List<&2, M.CmBlock>
871  {Pc.CrPcbc.decrypt_blocks(~Tf.LcTwofishKey, ~M.CmBlock, ~Tf.LcTwofish.decrypt, ~CM.CrBlk128.xor, k, iv, Pc.CrPcbc.encrypt_blocks(~Tf.LcTwofishKey, ~M.CmBlock, ~Tf.LcTwofish.encrypt, ~CM.CrBlk128.xor, k, iv, bs)) == bs : List<&2, M.CmBlock>}
872
873# Twofish (legacy-ciphers) in LRW (lrw.bend): decryption undoes encryption, for every key, tweak key, index and list of blocks
874law twofish_lrw_round_trip:
875  for +k: Tf.LcTwofishKey
876  for +k2: G.Gf128
877  for +i: G.Gf128
878  for +bs: List<&2, M.CmBlock>
879  {Lw.CrLrw.decrypt_blocks(~Tf.LcTwofishKey, ~M.CmBlock, ~Tf.LcTwofish.decrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, k, k2, i, Lw.CrLrw.encrypt_blocks(~Tf.LcTwofishKey, ~M.CmBlock, ~Tf.LcTwofish.encrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, k, k2, i, bs)) == bs : List<&2, M.CmBlock>}
880
881# ARIA (legacy-ciphers): decryption undoes encryption, for every key and block
882law aria_block_round_trip:
883  for k: Ar.LcAriaKey
884  for +b: M.CmBlock
885  {Ar.LcAria.decrypt(k, Ar.LcAria.encrypt(k, b)) == b : M.CmBlock}
886
887# ARIA (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
888law aria_block_round_trip_dual:
889  for k: Ar.LcAriaKey
890  for +b: M.CmBlock
891  {Ar.LcAria.encrypt(k, Ar.LcAria.decrypt(k, b)) == b : M.CmBlock}
892
893# ARIA (legacy-ciphers): a key of 20 bytes is refused
894law aria_key_length:
895  {Result.map(&2, &2, Cr.CrError, Ar.LcAriaKey, Unit, k => Unit{}, LC.CrLc.key(~Ar.LcAriaKey, ~Ar.LcAria.key, B.Octets.zeros(20n))) == Fail{Cr.CrBadKeyLength{20n}} : Result<&2, &2, Cr.CrError, Unit>}
896
897# ARIA (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
898law aria_ecb_round_trip:
899  for +k: Ar.LcAriaKey
900  for +bs: List<&2, M.CmBlock>
901  {Md.CrEcb.decrypt_blocks(~Ar.LcAriaKey, ~M.CmBlock, ~Ar.LcAria.decrypt, k, Md.CrEcb.encrypt_blocks(~Ar.LcAriaKey, ~M.CmBlock, ~Ar.LcAria.encrypt, k, bs)) == bs : List<&2, M.CmBlock>}
902
903# ARIA (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
904law aria_cbc_round_trip:
905  for +k: Ar.LcAriaKey
906  for +iv: M.CmBlock
907  for +bs: List<&2, M.CmBlock>
908  {Md.CrCbc.decrypt_blocks(~Ar.LcAriaKey, ~M.CmBlock, ~Ar.LcAria.decrypt, ~CM.CrBlk128.xor, k, iv, Md.CrCbc.encrypt_blocks(~Ar.LcAriaKey, ~M.CmBlock, ~Ar.LcAria.encrypt, ~CM.CrBlk128.xor, k, iv, bs)) == bs : List<&2, M.CmBlock>}
909
910# ARIA (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
911law aria_pcbc_round_trip:
912  for +k: Ar.LcAriaKey
913  for +iv: M.CmBlock
914  for +bs: List<&2, M.CmBlock>
915  {Pc.CrPcbc.decrypt_blocks(~Ar.LcAriaKey, ~M.CmBlock, ~Ar.LcAria.decrypt, ~CM.CrBlk128.xor, k, iv, Pc.CrPcbc.encrypt_blocks(~Ar.LcAriaKey, ~M.CmBlock, ~Ar.LcAria.encrypt, ~CM.CrBlk128.xor, k, iv, bs)) == bs : List<&2, M.CmBlock>}
916
917# ARIA (legacy-ciphers) in LRW (lrw.bend): decryption undoes encryption, for every key, tweak key, index and list of blocks
918law aria_lrw_round_trip:
919  for +k: Ar.LcAriaKey
920  for +k2: G.Gf128
921  for +i: G.Gf128
922  for +bs: List<&2, M.CmBlock>
923  {Lw.CrLrw.decrypt_blocks(~Ar.LcAriaKey, ~M.CmBlock, ~Ar.LcAria.decrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, k, k2, i, Lw.CrLrw.encrypt_blocks(~Ar.LcAriaKey, ~M.CmBlock, ~Ar.LcAria.encrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, k, k2, i, bs)) == bs : List<&2, M.CmBlock>}
924
925# CAST-256 (legacy-ciphers): decryption undoes encryption, for every key and block
926law cast6_block_round_trip:
927  for k: C6.LcCast6Key
928  for +b: M.CmBlock
929  {C6.LcCast6.decrypt(k, C6.LcCast6.encrypt(k, b)) == b : M.CmBlock}
930
931# CAST-256 (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
932law cast6_block_round_trip_dual:
933  for k: C6.LcCast6Key
934  for +b: M.CmBlock
935  {C6.LcCast6.encrypt(k, C6.LcCast6.decrypt(k, b)) == b : M.CmBlock}
936
937# CAST-256 (legacy-ciphers): a key of 18 bytes is refused
938law cast6_key_length:
939  {Result.map(&2, &2, Cr.CrError, C6.LcCast6Key, Unit, k => Unit{}, LC.CrLc.key(~C6.LcCast6Key, ~C6.LcCast6.key, B.Octets.zeros(18n))) == Fail{Cr.CrBadKeyLength{18n}} : Result<&2, &2, Cr.CrError, Unit>}
940
941# CAST-256 (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
942law cast6_ecb_round_trip:
943  for +k: C6.LcCast6Key
944  for +bs: List<&2, M.CmBlock>
945  {Md.CrEcb.decrypt_blocks(~C6.LcCast6Key, ~M.CmBlock, ~C6.LcCast6.decrypt, k, Md.CrEcb.encrypt_blocks(~C6.LcCast6Key, ~M.CmBlock, ~C6.LcCast6.encrypt, k, bs)) == bs : List<&2, M.CmBlock>}
946
947# CAST-256 (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
948law cast6_cbc_round_trip:
949  for +k: C6.LcCast6Key
950  for +iv: M.CmBlock
951  for +bs: List<&2, M.CmBlock>
952  {Md.CrCbc.decrypt_blocks(~C6.LcCast6Key, ~M.CmBlock, ~C6.LcCast6.decrypt, ~CM.CrBlk128.xor, k, iv, Md.CrCbc.encrypt_blocks(~C6.LcCast6Key, ~M.CmBlock, ~C6.LcCast6.encrypt, ~CM.CrBlk128.xor, k, iv, bs)) == bs : List<&2, M.CmBlock>}
953
954# CAST-256 (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
955law cast6_pcbc_round_trip:
956  for +k: C6.LcCast6Key
957  for +iv: M.CmBlock
958  for +bs: List<&2, M.CmBlock>
959  {Pc.CrPcbc.decrypt_blocks(~C6.LcCast6Key, ~M.CmBlock, ~C6.LcCast6.decrypt, ~CM.CrBlk128.xor, k, iv, Pc.CrPcbc.encrypt_blocks(~C6.LcCast6Key, ~M.CmBlock, ~C6.LcCast6.encrypt, ~CM.CrBlk128.xor, k, iv, bs)) == bs : List<&2, M.CmBlock>}
960
961# CAST-256 (legacy-ciphers) in LRW (lrw.bend): decryption undoes encryption, for every key, tweak key, index and list of blocks
962law cast6_lrw_round_trip:
963  for +k: C6.LcCast6Key
964  for +k2: G.Gf128
965  for +i: G.Gf128
966  for +bs: List<&2, M.CmBlock>
967  {Lw.CrLrw.decrypt_blocks(~C6.LcCast6Key, ~M.CmBlock, ~C6.LcCast6.decrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, k, k2, i, Lw.CrLrw.encrypt_blocks(~C6.LcCast6Key, ~M.CmBlock, ~C6.LcCast6.encrypt, ~CM.CrBlk128.xor, ~CM.CrBlk128.of_octets, k, k2, i, bs)) == bs : List<&2, M.CmBlock>}
968
969# Blowfish (legacy-ciphers): decryption undoes encryption, for every key and block
970law blowfish_block_round_trip:
971  for k: Bf.LcBlowfishKey
972  for +b: L.LcBlock64
973  {Bf.LcBlowfish.decrypt(k, Bf.LcBlowfish.encrypt(k, b)) == b : L.LcBlock64}
974
975# Blowfish (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
976law blowfish_block_round_trip_dual:
977  for k: Bf.LcBlowfishKey
978  for +b: L.LcBlock64
979  {Bf.LcBlowfish.encrypt(k, Bf.LcBlowfish.decrypt(k, b)) == b : L.LcBlock64}
980
981# Blowfish (legacy-ciphers): a key of 3 bytes is refused
982law blowfish_key_length:
983  {Result.map(&2, &2, Cr.CrError, Bf.LcBlowfishKey, Unit, k => Unit{}, LC.CrLc.key(~Bf.LcBlowfishKey, ~Bf.LcBlowfish.key, B.Octets.zeros(3n))) == Fail{Cr.CrBadKeyLength{3n}} : Result<&2, &2, Cr.CrError, Unit>}
984
985# Blowfish (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
986law blowfish_ecb_round_trip:
987  for +k: Bf.LcBlowfishKey
988  for +bs: List<&2, L.LcBlock64>
989  {Md.CrEcb.decrypt_blocks(~Bf.LcBlowfishKey, ~L.LcBlock64, ~Bf.LcBlowfish.decrypt, k, Md.CrEcb.encrypt_blocks(~Bf.LcBlowfishKey, ~L.LcBlock64, ~Bf.LcBlowfish.encrypt, k, bs)) == bs : List<&2, L.LcBlock64>}
990
991# Blowfish (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
992law blowfish_cbc_round_trip:
993  for +k: Bf.LcBlowfishKey
994  for +iv: L.LcBlock64
995  for +bs: List<&2, L.LcBlock64>
996  {Md.CrCbc.decrypt_blocks(~Bf.LcBlowfishKey, ~L.LcBlock64, ~Bf.LcBlowfish.decrypt, ~LC.CrBlk64.xor, k, iv, Md.CrCbc.encrypt_blocks(~Bf.LcBlowfishKey, ~L.LcBlock64, ~Bf.LcBlowfish.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
997
998# Blowfish (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
999law blowfish_pcbc_round_trip:
1000  for +k: Bf.LcBlowfishKey
1001  for +iv: L.LcBlock64
1002  for +bs: List<&2, L.LcBlock64>
1003  {Pc.CrPcbc.decrypt_blocks(~Bf.LcBlowfishKey, ~L.LcBlock64, ~Bf.LcBlowfish.decrypt, ~LC.CrBlk64.xor, k, iv, Pc.CrPcbc.encrypt_blocks(~Bf.LcBlowfishKey, ~L.LcBlock64, ~Bf.LcBlowfish.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
1004
1005# CAST-128 (legacy-ciphers): decryption undoes encryption, for every key and block
1006law cast5_block_round_trip:
1007  for k: C5.LcCast5Key
1008  for +b: L.LcBlock64
1009  {C5.LcCast5.decrypt(k, C5.LcCast5.encrypt(k, b)) == b : L.LcBlock64}
1010
1011# CAST-128 (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
1012law cast5_block_round_trip_dual:
1013  for k: C5.LcCast5Key
1014  for +b: L.LcBlock64
1015  {C5.LcCast5.encrypt(k, C5.LcCast5.decrypt(k, b)) == b : L.LcBlock64}
1016
1017# CAST-128 (legacy-ciphers): a key of 4 bytes is refused
1018law cast5_key_length:
1019  {Result.map(&2, &2, Cr.CrError, C5.LcCast5Key, Unit, k => Unit{}, LC.CrLc.key(~C5.LcCast5Key, ~C5.LcCast5.key, B.Octets.zeros(4n))) == Fail{Cr.CrBadKeyLength{4n}} : Result<&2, &2, Cr.CrError, Unit>}
1020
1021# CAST-128 (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
1022law cast5_ecb_round_trip:
1023  for +k: C5.LcCast5Key
1024  for +bs: List<&2, L.LcBlock64>
1025  {Md.CrEcb.decrypt_blocks(~C5.LcCast5Key, ~L.LcBlock64, ~C5.LcCast5.decrypt, k, Md.CrEcb.encrypt_blocks(~C5.LcCast5Key, ~L.LcBlock64, ~C5.LcCast5.encrypt, k, bs)) == bs : List<&2, L.LcBlock64>}
1026
1027# CAST-128 (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
1028law cast5_cbc_round_trip:
1029  for +k: C5.LcCast5Key
1030  for +iv: L.LcBlock64
1031  for +bs: List<&2, L.LcBlock64>
1032  {Md.CrCbc.decrypt_blocks(~C5.LcCast5Key, ~L.LcBlock64, ~C5.LcCast5.decrypt, ~LC.CrBlk64.xor, k, iv, Md.CrCbc.encrypt_blocks(~C5.LcCast5Key, ~L.LcBlock64, ~C5.LcCast5.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
1033
1034# CAST-128 (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
1035law cast5_pcbc_round_trip:
1036  for +k: C5.LcCast5Key
1037  for +iv: L.LcBlock64
1038  for +bs: List<&2, L.LcBlock64>
1039  {Pc.CrPcbc.decrypt_blocks(~C5.LcCast5Key, ~L.LcBlock64, ~C5.LcCast5.decrypt, ~LC.CrBlk64.xor, k, iv, Pc.CrPcbc.encrypt_blocks(~C5.LcCast5Key, ~L.LcBlock64, ~C5.LcCast5.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
1040
1041# TEA, little-endian words (legacy-ciphers): decryption undoes encryption, for every key and block
1042law tea_block_round_trip:
1043  for k: Te.LcTeaKey
1044  for +b: L.LcBlock64
1045  {Te.LcTea.decrypt(k, Te.LcTea.encrypt(k, b)) == b : L.LcBlock64}
1046
1047# TEA, little-endian words (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
1048law tea_block_round_trip_dual:
1049  for k: Te.LcTeaKey
1050  for +b: L.LcBlock64
1051  {Te.LcTea.encrypt(k, Te.LcTea.decrypt(k, b)) == b : L.LcBlock64}
1052
1053# TEA, little-endian words (legacy-ciphers): a key of 15 bytes is refused
1054law tea_key_length:
1055  {Result.map(&2, &2, Cr.CrError, Te.LcTeaKey, Unit, k => Unit{}, LC.CrLc.key(~Te.LcTeaKey, ~Te.LcTea.key, B.Octets.zeros(15n))) == Fail{Cr.CrBadKeyLength{15n}} : Result<&2, &2, Cr.CrError, Unit>}
1056
1057# TEA, little-endian words (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
1058law tea_ecb_round_trip:
1059  for +k: Te.LcTeaKey
1060  for +bs: List<&2, L.LcBlock64>
1061  {Md.CrEcb.decrypt_blocks(~Te.LcTeaKey, ~L.LcBlock64, ~Te.LcTea.decrypt, k, Md.CrEcb.encrypt_blocks(~Te.LcTeaKey, ~L.LcBlock64, ~Te.LcTea.encrypt, k, bs)) == bs : List<&2, L.LcBlock64>}
1062
1063# TEA, little-endian words (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
1064law tea_cbc_round_trip:
1065  for +k: Te.LcTeaKey
1066  for +iv: L.LcBlock64
1067  for +bs: List<&2, L.LcBlock64>
1068  {Md.CrCbc.decrypt_blocks(~Te.LcTeaKey, ~L.LcBlock64, ~Te.LcTea.decrypt, ~LC.CrBlk64.xor, k, iv, Md.CrCbc.encrypt_blocks(~Te.LcTeaKey, ~L.LcBlock64, ~Te.LcTea.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
1069
1070# TEA, little-endian words (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
1071law tea_pcbc_round_trip:
1072  for +k: Te.LcTeaKey
1073  for +iv: L.LcBlock64
1074  for +bs: List<&2, L.LcBlock64>
1075  {Pc.CrPcbc.decrypt_blocks(~Te.LcTeaKey, ~L.LcBlock64, ~Te.LcTea.decrypt, ~LC.CrBlk64.xor, k, iv, Pc.CrPcbc.encrypt_blocks(~Te.LcTeaKey, ~L.LcBlock64, ~Te.LcTea.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
1076
1077# XTEA, little-endian words (legacy-ciphers): decryption undoes encryption, for every key and block
1078law xtea_block_round_trip:
1079  for k: Xt.LcXteaKey
1080  for +b: L.LcBlock64
1081  {Xt.LcXtea.decrypt(k, Xt.LcXtea.encrypt(k, b)) == b : L.LcBlock64}
1082
1083# XTEA, little-endian words (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
1084law xtea_block_round_trip_dual:
1085  for k: Xt.LcXteaKey
1086  for +b: L.LcBlock64
1087  {Xt.LcXtea.encrypt(k, Xt.LcXtea.decrypt(k, b)) == b : L.LcBlock64}
1088
1089# XTEA, little-endian words (legacy-ciphers): a key of 17 bytes is refused
1090law xtea_key_length:
1091  {Result.map(&2, &2, Cr.CrError, Xt.LcXteaKey, Unit, k => Unit{}, LC.CrLc.key(~Xt.LcXteaKey, ~Xt.LcXtea.key, B.Octets.zeros(17n))) == Fail{Cr.CrBadKeyLength{17n}} : Result<&2, &2, Cr.CrError, Unit>}
1092
1093# XTEA, little-endian words (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
1094law xtea_ecb_round_trip:
1095  for +k: Xt.LcXteaKey
1096  for +bs: List<&2, L.LcBlock64>
1097  {Md.CrEcb.decrypt_blocks(~Xt.LcXteaKey, ~L.LcBlock64, ~Xt.LcXtea.decrypt, k, Md.CrEcb.encrypt_blocks(~Xt.LcXteaKey, ~L.LcBlock64, ~Xt.LcXtea.encrypt, k, bs)) == bs : List<&2, L.LcBlock64>}
1098
1099# XTEA, little-endian words (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
1100law xtea_cbc_round_trip:
1101  for +k: Xt.LcXteaKey
1102  for +iv: L.LcBlock64
1103  for +bs: List<&2, L.LcBlock64>
1104  {Md.CrCbc.decrypt_blocks(~Xt.LcXteaKey, ~L.LcBlock64, ~Xt.LcXtea.decrypt, ~LC.CrBlk64.xor, k, iv, Md.CrCbc.encrypt_blocks(~Xt.LcXteaKey, ~L.LcBlock64, ~Xt.LcXtea.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
1105
1106# XTEA, little-endian words (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
1107law xtea_pcbc_round_trip:
1108  for +k: Xt.LcXteaKey
1109  for +iv: L.LcBlock64
1110  for +bs: List<&2, L.LcBlock64>
1111  {Pc.CrPcbc.decrypt_blocks(~Xt.LcXteaKey, ~L.LcBlock64, ~Xt.LcXtea.decrypt, ~LC.CrBlk64.xor, k, iv, Pc.CrPcbc.encrypt_blocks(~Xt.LcXteaKey, ~L.LcBlock64, ~Xt.LcXtea.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
1112
1113# FCrypt (legacy-ciphers): decryption undoes encryption, for every key and block
1114law fcrypt_block_round_trip:
1115  for k: Fc.LcFcryptKey
1116  for +b: L.LcBlock64
1117  {Fc.LcFcrypt.decrypt(k, Fc.LcFcrypt.encrypt(k, b)) == b : L.LcBlock64}
1118
1119# FCrypt (legacy-ciphers): encryption undoes decryption (a permutation of the blocks)
1120law fcrypt_block_round_trip_dual:
1121  for k: Fc.LcFcryptKey
1122  for +b: L.LcBlock64
1123  {Fc.LcFcrypt.encrypt(k, Fc.LcFcrypt.decrypt(k, b)) == b : L.LcBlock64}
1124
1125# FCrypt (legacy-ciphers): a key of 7 bytes is refused
1126law fcrypt_key_length:
1127  {Result.map(&2, &2, Cr.CrError, Fc.LcFcryptKey, Unit, k => Unit{}, LC.CrLc.key(~Fc.LcFcryptKey, ~Fc.LcFcrypt.key, B.Octets.zeros(7n))) == Fail{Cr.CrBadKeyLength{7n}} : Result<&2, &2, Cr.CrError, Unit>}
1128
1129# FCrypt (legacy-ciphers) in ECB (modes.bend): decryption undoes encryption, for every key and list of blocks
1130law fcrypt_ecb_round_trip:
1131  for +k: Fc.LcFcryptKey
1132  for +bs: List<&2, L.LcBlock64>
1133  {Md.CrEcb.decrypt_blocks(~Fc.LcFcryptKey, ~L.LcBlock64, ~Fc.LcFcrypt.decrypt, k, Md.CrEcb.encrypt_blocks(~Fc.LcFcryptKey, ~L.LcBlock64, ~Fc.LcFcrypt.encrypt, k, bs)) == bs : List<&2, L.LcBlock64>}
1134
1135# FCrypt (legacy-ciphers) in CBC (modes.bend): decryption undoes encryption, for every key, IV and list of blocks
1136law fcrypt_cbc_round_trip:
1137  for +k: Fc.LcFcryptKey
1138  for +iv: L.LcBlock64
1139  for +bs: List<&2, L.LcBlock64>
1140  {Md.CrCbc.decrypt_blocks(~Fc.LcFcryptKey, ~L.LcBlock64, ~Fc.LcFcrypt.decrypt, ~LC.CrBlk64.xor, k, iv, Md.CrCbc.encrypt_blocks(~Fc.LcFcryptKey, ~L.LcBlock64, ~Fc.LcFcrypt.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
1141
1142# FCrypt (legacy-ciphers) in PCBC (pcbc.bend): decryption undoes encryption, for every key, IV and list of blocks
1143law fcrypt_pcbc_round_trip:
1144  for +k: Fc.LcFcryptKey
1145  for +iv: L.LcBlock64
1146  for +bs: List<&2, L.LcBlock64>
1147  {Pc.CrPcbc.decrypt_blocks(~Fc.LcFcryptKey, ~L.LcBlock64, ~Fc.LcFcrypt.decrypt, ~LC.CrBlk64.xor, k, iv, Pc.CrPcbc.encrypt_blocks(~Fc.LcFcryptKey, ~L.LcBlock64, ~Fc.LcFcrypt.encrypt, ~LC.CrBlk64.xor, k, iv, bs)) == bs : List<&2, L.LcBlock64>}
1148
1149# AES-128 and AES-256 (cipher-modes): a key of 24 bytes is refused
1150law aes_key_length:
1151  {Result.map(&2, &2, Cr.CrError, X.CmAesKey, Unit, k => Unit{}, A.CrAes.key(B.Octets.zeros(24n))) == Fail{Cr.CrBadKeyLength{24n}} : Result<&2, &2, Cr.CrError, Unit>}
1152
1153# AES, encryption key schedule only (cipher-modes): a key of 20 bytes is refused
1154law aes_enc_key_length:
1155  {Result.map(&2, &2, Cr.CrError, X.CmAesKey, Unit, k => Unit{}, A.CrAes.key_enc(B.Octets.zeros(20n))) == Fail{Cr.CrBadKeyLength{20n}} : Result<&2, &2, Cr.CrError, Unit>}
1156
1157# RC4 (legacy-ciphers): from one state, applied twice, the data comes back
1158law rc4_stream_involution:
1159  for +s: R.LcRc4State
1160  for +m: B.Octets
1161  {R.LcRc4.out_data(R.LcRc4.update(s, R.LcRc4.out_data(R.LcRc4.update(s, m)))) == m : B.Octets}
1162
1163# RC4 (legacy-ciphers): the output of a ++ b is the output of a, then of b from the state after a
1164law rc4_stream_streaming_data:
1165  for +s: R.LcRc4State
1166  for +a: B.Octets
1167  for +b: B.Octets
1168  {R.LcRc4.out_data(R.LcRc4.update(s, B.Octets.append(a, b))) == B.Octets.append(R.LcRc4.out_data(R.LcRc4.update(s, a)), R.LcRc4.out_data(R.LcRc4.update(R.LcRc4.out_state(R.LcRc4.update(s, a)), b))) : B.Octets}
1169
1170# RC4 (legacy-ciphers): the state after a ++ b is the state after a, then b
1171law rc4_stream_streaming_state:
1172  for +s: R.LcRc4State
1173  for +a: B.Octets
1174  for +b: B.Octets
1175  {R.LcRc4.out_state(R.LcRc4.update(s, B.Octets.append(a, b))) == R.LcRc4.out_state(R.LcRc4.update(R.LcRc4.out_state(R.LcRc4.update(s, a)), b)) : R.LcRc4State}
1176
1177# HMAC over CRC-32 of any parameter set (crc): the state after a ++ b is the state after a, then b
1178law hmac_crc32_streaming:
1179  for ~spec: C.Crc32Spec
1180  for s: Hm.CrHmacState<U32>
1181  for +a: B.Octets
1182  for +b: B.Octets
1183  {Hm.CrHmac.update(~U32, ~CR.CrCrc32.update(~spec), s, B.Octets.append(a, b)) == Hm.CrHmac.update(~U32, ~CR.CrCrc32.update(~spec), Hm.CrHmac.update(~U32, ~CR.CrCrc32.update(~spec), s, a), b) : Hm.CrHmacState<U32>}
1184
1185# HMAC over CRC-32 of any parameter set (crc): the tag in pieces is the tag in one call, for every split
1186law hmac_crc32_split:
1187  for ~spec: C.Crc32Spec
1188  for +kk: Hm.CrHmacKey
1189  for +a: B.Octets
1190  for +b: B.Octets
1191  {Hm.CrHmac.finish(~U32, ~CR.CrCrc32.init(~spec), ~CR.CrCrc32.update(~spec), ~CR.CrCrc32.final(~spec), Hm.CrHmac.update(~U32, ~CR.CrCrc32.update(~spec), Hm.CrHmac.update(~U32, ~CR.CrCrc32.update(~spec), Hm.CrHmac.start(~U32, ~CR.CrCrc32.init(~spec), ~CR.CrCrc32.update(~spec), kk), a), b)) == Hm.CrHmac.mac(~CR.CrCrc32.digest(~spec), kk, B.Octets.append(a, b)) : B.Octets}
1192
1193# HMAC over CRC-64 of any parameter set (crc): the state after a ++ b is the state after a, then b
1194law hmac_crc64_streaming:
1195  for ~spec: C.Crc64Spec
1196  for s: Hm.CrHmacState<W.W64>
1197  for +a: B.Octets
1198  for +b: B.Octets
1199  {Hm.CrHmac.update(~W.W64, ~CR.CrCrc64.update(~spec), s, B.Octets.append(a, b)) == Hm.CrHmac.update(~W.W64, ~CR.CrCrc64.update(~spec), Hm.CrHmac.update(~W.W64, ~CR.CrCrc64.update(~spec), s, a), b) : Hm.CrHmacState<W.W64>}
1200
1201# HMAC over CRC-64 of any parameter set (crc): the tag in pieces is the tag in one call, for every split
1202law hmac_crc64_split:
1203  for ~spec: C.Crc64Spec
1204  for +kk: Hm.CrHmacKey
1205  for +a: B.Octets
1206  for +b: B.Octets
1207  {Hm.CrHmac.finish(~W.W64, ~CR.CrCrc64.init(~spec), ~CR.CrCrc64.update(~spec), ~CR.CrCrc64.final(~spec), Hm.CrHmac.update(~W.W64, ~CR.CrCrc64.update(~spec), Hm.CrHmac.update(~W.W64, ~CR.CrCrc64.update(~spec), Hm.CrHmac.start(~W.W64, ~CR.CrCrc64.init(~spec), ~CR.CrCrc64.update(~spec), kk), a), b)) == Hm.CrHmac.mac(~CR.CrCrc64.digest(~spec), kk, B.Octets.append(a, b)) : B.Octets}
1208
1209# HMAC over SHA-256 (bend-collections): the tag in pieces is the tag in one call, for every split
1210law hmac_sha256_split:
1211  for +kk: Hm.CrHmacKey
1212  for +a: B.Octets
1213  for +b: B.Octets
1214  {Hm.CrHmac.finish(~SH.CrSha2State, ~SH.CrSha2.init256(), ~SH.CrSha2.update, ~SH.CrSha2.final, Hm.CrHmac.update(~SH.CrSha2State, ~SH.CrSha2.update, Hm.CrHmac.update(~SH.CrSha2State, ~SH.CrSha2.update, Hm.CrHmac.start(~SH.CrSha2State, ~SH.CrSha2.init256(), ~SH.CrSha2.update, kk), a), b)) == Hm.CrHmac.mac(~SH.CrSha2.sha256, kk, B.Octets.append(a, b)) : B.Octets}
1215
1216# HMAC over SHA-512 (bend-collections): the tag in pieces is the tag in one call, for every split
1217law hmac_sha512_split:
1218  for +kk: Hm.CrHmacKey
1219  for +a: B.Octets
1220  for +b: B.Octets
1221  {Hm.CrHmac.finish(~SH.CrSha2State, ~SH.CrSha2.init512(), ~SH.CrSha2.update, ~SH.CrSha2.final, Hm.CrHmac.update(~SH.CrSha2State, ~SH.CrSha2.update, Hm.CrHmac.update(~SH.CrSha2State, ~SH.CrSha2.update, Hm.CrHmac.start(~SH.CrSha2State, ~SH.CrSha2.init512(), ~SH.CrSha2.update, kk), a), b)) == Hm.CrHmac.mac(~SH.CrSha2.sha512, kk, B.Octets.append(a, b)) : B.Octets}
1222
1223# HMAC over SHA3-256 (bend-collections): the tag in pieces is the tag in one call, for every split
1224law hmac_sha3_256_split:
1225  for +kk: Hm.CrHmacKey
1226  for +a: B.Octets
1227  for +b: B.Octets
1228  {Hm.CrHmac.finish(~S3.CrSha3State, ~S3.CrSha3.init(), ~S3.CrSha3.update, ~S3.CrSha3.final, Hm.CrHmac.update(~S3.CrSha3State, ~S3.CrSha3.update, Hm.CrHmac.update(~S3.CrSha3State, ~S3.CrSha3.update, Hm.CrHmac.start(~S3.CrSha3State, ~S3.CrSha3.init(), ~S3.CrSha3.update, kk), a), b)) == Hm.CrHmac.mac(~S3.CrSha3.sha3_256, kk, B.Octets.append(a, b)) : B.Octets}
1229
1230# MD4 (hashes): update over a ++ b is update over a, then b, for every state
1231law md4_hash_streaming:
1232  for s: Hs.HsMdState<Hs.HsW4>
1233  for +a: B.Octets
1234  for +b: B.Octets
1235  {HM4.HsMd4.update(s, B.Octets.append(a, b)) == HM4.HsMd4.update(HM4.HsMd4.update(s, a), b) : Hs.HsMdState<Hs.HsW4>}
1236
1237# MD4 (hashes): streaming equals one-shot, for every split
1238law md4_hash_split:
1239  for +a: B.Octets
1240  for +b: B.Octets
1241  {HM4.HsMd4.final(HM4.HsMd4.update(HM4.HsMd4.update(HM4.HsMd4.init(), a), b)) == HM4.HsMd4.digest(B.Octets.append(a, b)) : B.Octets}
1242
1243# MD4 (hashes): and for every split into three
1244law md4_hash_split3:
1245  for +a: B.Octets
1246  for +b: B.Octets
1247  for +c: B.Octets
1248  {HM4.HsMd4.final(HM4.HsMd4.update(HM4.HsMd4.update(HM4.HsMd4.update(HM4.HsMd4.init(), a), b), c)) == HM4.HsMd4.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
1249
1250# MD4 (hashes): final(s) has 16 bytes, for every state
1251law md4_hash_length:
1252  for +s: Hs.HsMdState<Hs.HsW4>
1253  {B.Octets.len(HM4.HsMd4.final(s)) == 16n : Nat}
1254
1255# HMAC over MD4 (hashes): the state after a ++ b is the state after a, then b
1256law hmac_md4_streaming:
1257  for s: Hm.CrHmacState<Hs.HsMdState<Hs.HsW4>>
1258  for +a: B.Octets
1259  for +b: B.Octets
1260  {Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW4>, ~HM4.HsMd4.update, s, B.Octets.append(a, b)) == Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW4>, ~HM4.HsMd4.update, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW4>, ~HM4.HsMd4.update, s, a), b) : Hm.CrHmacState<Hs.HsMdState<Hs.HsW4>>}
1261
1262# HMAC over MD4 (hashes): the tag in pieces is the tag in one call, for every split
1263law hmac_md4_split:
1264  for +kk: Hm.CrHmacKey
1265  for +a: B.Octets
1266  for +b: B.Octets
1267  {Hm.CrHmac.finish(~Hs.HsMdState<Hs.HsW4>, ~HM4.HsMd4.init(), ~HM4.HsMd4.update, ~HM4.HsMd4.final, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW4>, ~HM4.HsMd4.update, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW4>, ~HM4.HsMd4.update, Hm.CrHmac.start(~Hs.HsMdState<Hs.HsW4>, ~HM4.HsMd4.init(), ~HM4.HsMd4.update, kk), a), b)) == Hm.CrHmac.mac(~HM4.HsMd4.digest, kk, B.Octets.append(a, b)) : B.Octets}
1268
1269# MD5 (hashes): update over a ++ b is update over a, then b, for every state
1270law md5_hash_streaming:
1271  for s: Hs.HsMdState<Hs.HsW4>
1272  for +a: B.Octets
1273  for +b: B.Octets
1274  {HM5.HsMd5.update(s, B.Octets.append(a, b)) == HM5.HsMd5.update(HM5.HsMd5.update(s, a), b) : Hs.HsMdState<Hs.HsW4>}
1275
1276# MD5 (hashes): streaming equals one-shot, for every split
1277law md5_hash_split:
1278  for +a: B.Octets
1279  for +b: B.Octets
1280  {HM5.HsMd5.final(HM5.HsMd5.update(HM5.HsMd5.update(HM5.HsMd5.init(), a), b)) == HM5.HsMd5.digest(B.Octets.append(a, b)) : B.Octets}
1281
1282# MD5 (hashes): and for every split into three
1283law md5_hash_split3:
1284  for +a: B.Octets
1285  for +b: B.Octets
1286  for +c: B.Octets
1287  {HM5.HsMd5.final(HM5.HsMd5.update(HM5.HsMd5.update(HM5.HsMd5.update(HM5.HsMd5.init(), a), b), c)) == HM5.HsMd5.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
1288
1289# MD5 (hashes): final(s) has 16 bytes, for every state
1290law md5_hash_length:
1291  for +s: Hs.HsMdState<Hs.HsW4>
1292  {B.Octets.len(HM5.HsMd5.final(s)) == 16n : Nat}
1293
1294# HMAC over MD5 (hashes): the state after a ++ b is the state after a, then b
1295law hmac_md5_streaming:
1296  for s: Hm.CrHmacState<Hs.HsMdState<Hs.HsW4>>
1297  for +a: B.Octets
1298  for +b: B.Octets
1299  {Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW4>, ~HM5.HsMd5.update, s, B.Octets.append(a, b)) == Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW4>, ~HM5.HsMd5.update, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW4>, ~HM5.HsMd5.update, s, a), b) : Hm.CrHmacState<Hs.HsMdState<Hs.HsW4>>}
1300
1301# HMAC over MD5 (hashes): the tag in pieces is the tag in one call, for every split
1302law hmac_md5_split:
1303  for +kk: Hm.CrHmacKey
1304  for +a: B.Octets
1305  for +b: B.Octets
1306  {Hm.CrHmac.finish(~Hs.HsMdState<Hs.HsW4>, ~HM5.HsMd5.init(), ~HM5.HsMd5.update, ~HM5.HsMd5.final, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW4>, ~HM5.HsMd5.update, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW4>, ~HM5.HsMd5.update, Hm.CrHmac.start(~Hs.HsMdState<Hs.HsW4>, ~HM5.HsMd5.init(), ~HM5.HsMd5.update, kk), a), b)) == Hm.CrHmac.mac(~HM5.HsMd5.digest, kk, B.Octets.append(a, b)) : B.Octets}
1307
1308# SHA-1 (hashes): update over a ++ b is update over a, then b, for every state
1309law sha1_hash_streaming:
1310  for s: Hs.HsMdState<Hs.HsW5>
1311  for +a: B.Octets
1312  for +b: B.Octets
1313  {HS1.HsSha1.update(s, B.Octets.append(a, b)) == HS1.HsSha1.update(HS1.HsSha1.update(s, a), b) : Hs.HsMdState<Hs.HsW5>}
1314
1315# SHA-1 (hashes): streaming equals one-shot, for every split
1316law sha1_hash_split:
1317  for +a: B.Octets
1318  for +b: B.Octets
1319  {HS1.HsSha1.final(HS1.HsSha1.update(HS1.HsSha1.update(HS1.HsSha1.init(), a), b)) == HS1.HsSha1.digest(B.Octets.append(a, b)) : B.Octets}
1320
1321# SHA-1 (hashes): and for every split into three
1322law sha1_hash_split3:
1323  for +a: B.Octets
1324  for +b: B.Octets
1325  for +c: B.Octets
1326  {HS1.HsSha1.final(HS1.HsSha1.update(HS1.HsSha1.update(HS1.HsSha1.update(HS1.HsSha1.init(), a), b), c)) == HS1.HsSha1.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
1327
1328# SHA-1 (hashes): final(s) has 20 bytes, for every state
1329law sha1_hash_length:
1330  for +s: Hs.HsMdState<Hs.HsW5>
1331  {B.Octets.len(HS1.HsSha1.final(s)) == 20n : Nat}
1332
1333# HMAC over SHA-1 (hashes): the state after a ++ b is the state after a, then b
1334law hmac_sha1_streaming:
1335  for s: Hm.CrHmacState<Hs.HsMdState<Hs.HsW5>>
1336  for +a: B.Octets
1337  for +b: B.Octets
1338  {Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW5>, ~HS1.HsSha1.update, s, B.Octets.append(a, b)) == Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW5>, ~HS1.HsSha1.update, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW5>, ~HS1.HsSha1.update, s, a), b) : Hm.CrHmacState<Hs.HsMdState<Hs.HsW5>>}
1339
1340# HMAC over SHA-1 (hashes): the tag in pieces is the tag in one call, for every split
1341law hmac_sha1_split:
1342  for +kk: Hm.CrHmacKey
1343  for +a: B.Octets
1344  for +b: B.Octets
1345  {Hm.CrHmac.finish(~Hs.HsMdState<Hs.HsW5>, ~HS1.HsSha1.init(), ~HS1.HsSha1.update, ~HS1.HsSha1.final, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW5>, ~HS1.HsSha1.update, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW5>, ~HS1.HsSha1.update, Hm.CrHmac.start(~Hs.HsMdState<Hs.HsW5>, ~HS1.HsSha1.init(), ~HS1.HsSha1.update, kk), a), b)) == Hm.CrHmac.mac(~HS1.HsSha1.digest, kk, B.Octets.append(a, b)) : B.Octets}
1346
1347# RIPEMD-160 (hashes): update over a ++ b is update over a, then b, for every state
1348law ripemd160_hash_streaming:
1349  for s: Hs.HsMdState<Hs.HsW5>
1350  for +a: B.Octets
1351  for +b: B.Octets
1352  {HRM.HsRipemd160.update(s, B.Octets.append(a, b)) == HRM.HsRipemd160.update(HRM.HsRipemd160.update(s, a), b) : Hs.HsMdState<Hs.HsW5>}
1353
1354# RIPEMD-160 (hashes): streaming equals one-shot, for every split
1355law ripemd160_hash_split:
1356  for +a: B.Octets
1357  for +b: B.Octets
1358  {HRM.HsRipemd160.final(HRM.HsRipemd160.update(HRM.HsRipemd160.update(HRM.HsRipemd160.init(), a), b)) == HRM.HsRipemd160.digest(B.Octets.append(a, b)) : B.Octets}
1359
1360# RIPEMD-160 (hashes): and for every split into three
1361law ripemd160_hash_split3:
1362  for +a: B.Octets
1363  for +b: B.Octets
1364  for +c: B.Octets
1365  {HRM.HsRipemd160.final(HRM.HsRipemd160.update(HRM.HsRipemd160.update(HRM.HsRipemd160.update(HRM.HsRipemd160.init(), a), b), c)) == HRM.HsRipemd160.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
1366
1367# RIPEMD-160 (hashes): final(s) has 20 bytes, for every state
1368law ripemd160_hash_length:
1369  for +s: Hs.HsMdState<Hs.HsW5>
1370  {B.Octets.len(HRM.HsRipemd160.final(s)) == 20n : Nat}
1371
1372# HMAC over RIPEMD-160 (hashes): the state after a ++ b is the state after a, then b
1373law hmac_ripemd160_streaming:
1374  for s: Hm.CrHmacState<Hs.HsMdState<Hs.HsW5>>
1375  for +a: B.Octets
1376  for +b: B.Octets
1377  {Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW5>, ~HRM.HsRipemd160.update, s, B.Octets.append(a, b)) == Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW5>, ~HRM.HsRipemd160.update, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW5>, ~HRM.HsRipemd160.update, s, a), b) : Hm.CrHmacState<Hs.HsMdState<Hs.HsW5>>}
1378
1379# HMAC over RIPEMD-160 (hashes): the tag in pieces is the tag in one call, for every split
1380law hmac_ripemd160_split:
1381  for +kk: Hm.CrHmacKey
1382  for +a: B.Octets
1383  for +b: B.Octets
1384  {Hm.CrHmac.finish(~Hs.HsMdState<Hs.HsW5>, ~HRM.HsRipemd160.init(), ~HRM.HsRipemd160.update, ~HRM.HsRipemd160.final, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW5>, ~HRM.HsRipemd160.update, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW5>, ~HRM.HsRipemd160.update, Hm.CrHmac.start(~Hs.HsMdState<Hs.HsW5>, ~HRM.HsRipemd160.init(), ~HRM.HsRipemd160.update, kk), a), b)) == Hm.CrHmac.mac(~HRM.HsRipemd160.digest, kk, B.Octets.append(a, b)) : B.Octets}
1385
1386# SM3 (hashes): update over a ++ b is update over a, then b, for every state
1387law sm3_hash_streaming:
1388  for s: Hs.HsMdState<Hs.HsW8>
1389  for +a: B.Octets
1390  for +b: B.Octets
1391  {HSM.HsSm3.update(s, B.Octets.append(a, b)) == HSM.HsSm3.update(HSM.HsSm3.update(s, a), b) : Hs.HsMdState<Hs.HsW8>}
1392
1393# SM3 (hashes): streaming equals one-shot, for every split
1394law sm3_hash_split:
1395  for +a: B.Octets
1396  for +b: B.Octets
1397  {HSM.HsSm3.final(HSM.HsSm3.update(HSM.HsSm3.update(HSM.HsSm3.init(), a), b)) == HSM.HsSm3.digest(B.Octets.append(a, b)) : B.Octets}
1398
1399# SM3 (hashes): and for every split into three
1400law sm3_hash_split3:
1401  for +a: B.Octets
1402  for +b: B.Octets
1403  for +c: B.Octets
1404  {HSM.HsSm3.final(HSM.HsSm3.update(HSM.HsSm3.update(HSM.HsSm3.update(HSM.HsSm3.init(), a), b), c)) == HSM.HsSm3.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
1405
1406# SM3 (hashes): final(s) has 32 bytes, for every state
1407law sm3_hash_length:
1408  for +s: Hs.HsMdState<Hs.HsW8>
1409  {B.Octets.len(HSM.HsSm3.final(s)) == 32n : Nat}
1410
1411# HMAC over SM3 (hashes): the state after a ++ b is the state after a, then b
1412law hmac_sm3_streaming:
1413  for s: Hm.CrHmacState<Hs.HsMdState<Hs.HsW8>>
1414  for +a: B.Octets
1415  for +b: B.Octets
1416  {Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW8>, ~HSM.HsSm3.update, s, B.Octets.append(a, b)) == Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW8>, ~HSM.HsSm3.update, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW8>, ~HSM.HsSm3.update, s, a), b) : Hm.CrHmacState<Hs.HsMdState<Hs.HsW8>>}
1417
1418# HMAC over SM3 (hashes): the tag in pieces is the tag in one call, for every split
1419law hmac_sm3_split:
1420  for +kk: Hm.CrHmacKey
1421  for +a: B.Octets
1422  for +b: B.Octets
1423  {Hm.CrHmac.finish(~Hs.HsMdState<Hs.HsW8>, ~HSM.HsSm3.init(), ~HSM.HsSm3.update, ~HSM.HsSm3.final, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW8>, ~HSM.HsSm3.update, Hm.CrHmac.update(~Hs.HsMdState<Hs.HsW8>, ~HSM.HsSm3.update, Hm.CrHmac.start(~Hs.HsMdState<Hs.HsW8>, ~HSM.HsSm3.init(), ~HSM.HsSm3.update, kk), a), b)) == Hm.CrHmac.mac(~HSM.HsSm3.digest, kk, B.Octets.append(a, b)) : B.Octets}
1424
1425# Streebog-256 (hashes): update over a ++ b is update over a, then b, for every state
1426law streebog256_hash_streaming:
1427  for s: Hs.HsMdState<HST.HsStbCv>
1428  for +a: B.Octets
1429  for +b: B.Octets
1430  {HST.HsStreebog.update(s, B.Octets.append(a, b)) == HST.HsStreebog.update(HST.HsStreebog.update(s, a), b) : Hs.HsMdState<HST.HsStbCv>}
1431
1432# Streebog-256 (hashes): streaming equals one-shot, for every split
1433law streebog256_hash_split:
1434  for +a: B.Octets
1435  for +b: B.Octets
1436  {HST.HsStreebog.final256(HST.HsStreebog.update(HST.HsStreebog.update(HST.HsStreebog.init256(), a), b)) == HST.HsStreebog.digest256(B.Octets.append(a, b)) : B.Octets}
1437
1438# Streebog-256 (hashes): and for every split into three
1439law streebog256_hash_split3:
1440  for +a: B.Octets
1441  for +b: B.Octets
1442  for +c: B.Octets
1443  {HST.HsStreebog.final256(HST.HsStreebog.update(HST.HsStreebog.update(HST.HsStreebog.update(HST.HsStreebog.init256(), a), b), c)) == HST.HsStreebog.digest256(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
1444
1445# Streebog-256 (hashes): final(s) has 32 bytes, for every state
1446law streebog256_hash_length:
1447  for +s: Hs.HsMdState<HST.HsStbCv>
1448  {B.Octets.len(HST.HsStreebog.final256(s)) == 32n : Nat}
1449
1450# HMAC over Streebog-256 (hashes): the state after a ++ b is the state after a, then b
1451law hmac_streebog256_streaming:
1452  for s: Hm.CrHmacState<Hs.HsMdState<HST.HsStbCv>>
1453  for +a: B.Octets
1454  for +b: B.Octets
1455  {Hm.CrHmac.update(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.update, s, B.Octets.append(a, b)) == Hm.CrHmac.update(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.update, Hm.CrHmac.update(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.update, s, a), b) : Hm.CrHmacState<Hs.HsMdState<HST.HsStbCv>>}
1456
1457# HMAC over Streebog-256 (hashes): the tag in pieces is the tag in one call, for every split
1458law hmac_streebog256_split:
1459  for +kk: Hm.CrHmacKey
1460  for +a: B.Octets
1461  for +b: B.Octets
1462  {Hm.CrHmac.finish(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.init256(), ~HST.HsStreebog.update, ~HST.HsStreebog.final256, Hm.CrHmac.update(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.update, Hm.CrHmac.update(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.update, Hm.CrHmac.start(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.init256(), ~HST.HsStreebog.update, kk), a), b)) == Hm.CrHmac.mac(~HST.HsStreebog.digest256, kk, B.Octets.append(a, b)) : B.Octets}
1463
1464# Streebog-512 (hashes): update over a ++ b is update over a, then b, for every state
1465law streebog512_hash_streaming:
1466  for s: Hs.HsMdState<HST.HsStbCv>
1467  for +a: B.Octets
1468  for +b: B.Octets
1469  {HST.HsStreebog.update(s, B.Octets.append(a, b)) == HST.HsStreebog.update(HST.HsStreebog.update(s, a), b) : Hs.HsMdState<HST.HsStbCv>}
1470
1471# Streebog-512 (hashes): streaming equals one-shot, for every split
1472law streebog512_hash_split:
1473  for +a: B.Octets
1474  for +b: B.Octets
1475  {HST.HsStreebog.final512(HST.HsStreebog.update(HST.HsStreebog.update(HST.HsStreebog.init512(), a), b)) == HST.HsStreebog.digest512(B.Octets.append(a, b)) : B.Octets}
1476
1477# Streebog-512 (hashes): and for every split into three
1478law streebog512_hash_split3:
1479  for +a: B.Octets
1480  for +b: B.Octets
1481  for +c: B.Octets
1482  {HST.HsStreebog.final512(HST.HsStreebog.update(HST.HsStreebog.update(HST.HsStreebog.update(HST.HsStreebog.init512(), a), b), c)) == HST.HsStreebog.digest512(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets}
1483
1484# Streebog-512 (hashes): final(s) has 64 bytes, for every state
1485law streebog512_hash_length:
1486  for +s: Hs.HsMdState<HST.HsStbCv>
1487  {B.Octets.len(HST.HsStreebog.final512(s)) == 64n : Nat}
1488
1489# HMAC over Streebog-512 (hashes): the state after a ++ b is the state after a, then b
1490law hmac_streebog512_streaming:
1491  for s: Hm.CrHmacState<Hs.HsMdState<HST.HsStbCv>>
1492  for +a: B.Octets
1493  for +b: B.Octets
1494  {Hm.CrHmac.update(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.update, s, B.Octets.append(a, b)) == Hm.CrHmac.update(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.update, Hm.CrHmac.update(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.update, s, a), b) : Hm.CrHmacState<Hs.HsMdState<HST.HsStbCv>>}
1495
1496# HMAC over Streebog-512 (hashes): the tag in pieces is the tag in one call, for every split
1497law hmac_streebog512_split:
1498  for +kk: Hm.CrHmacKey
1499  for +a: B.Octets
1500  for +b: B.Octets
1501  {Hm.CrHmac.finish(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.init512(), ~HST.HsStreebog.update, ~HST.HsStreebog.final512, Hm.CrHmac.update(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.update, Hm.CrHmac.update(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.update, Hm.CrHmac.start(~Hs.HsMdState<HST.HsStbCv>, ~HST.HsStreebog.init512(), ~HST.HsStreebog.update, kk), a), b)) == Hm.CrHmac.mac(~HST.HsStreebog.digest512, kk, B.Octets.append(a, b)) : B.Octets}
1502# END GENERATED: laws