law Block.value

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/laws.bend:67

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/aes.bend as A
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S

67# The byte API: a key of 16, 24 or 32 bytes encrypts a 16-byte block with
68# AES under the key's Nk = length/4 and Nr = Nk + 6 (FIPS 197 Figure 4).
69law Block.value:
70  for +key: List<&2, U32>
71  for +h: {A.valid_length(List.length(&2, U32, key)) == True{} : Bool}
72  for +b0: U32
73  for +b1: U32
74  for +b2: U32
75  for +b3: U32
76  for +b4: U32
77  for +b5: U32
78  for +b6: U32
79  for +b7: U32
80  for +b8: U32
81  for +b9: U32
82  for +b10: U32
83  for +b11: U32
84  for +b12: U32
85  for +b13: U32
86  for +b14: U32
87  for +b15: U32
88  {block_with(A.expand_key(key), [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15]) == Some{S.bytes_of(S.aes(key, S.state_of([b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15])))} : Maybe<&2, List<&2, U32>>}