def ks_ok

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

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

44def ks_ok(+st: T.State) -> {S.bytes_of(st) == [S.nth_byte(S.bytes_of(st), 0n), S.nth_byte(S.bytes_of(st), 1n), S.nth_byte(S.bytes_of(st), 2n), S.nth_byte(S.bytes_of(st), 3n), S.nth_byte(S.bytes_of(st), 4n), S.nth_byte(S.bytes_of(st), 5n), S.nth_byte(S.bytes_of(st), 6n), S.nth_byte(S.bytes_of(st), 7n), S.nth_byte(S.bytes_of(st), 8n), S.nth_byte(S.bytes_of(st), 9n), S.nth_byte(S.bytes_of(st), 10n), S.nth_byte(S.bytes_of(st), 11n), S.nth_byte(S.bytes_of(st), 12n), S.nth_byte(S.bytes_of(st), 13n), S.nth_byte(S.bytes_of(st), 14n), S.nth_byte(S.bytes_of(st), 15n)] : List<&2, U32>}:
45  match st:
46    case T.S{T.W{a0, a1, a2, a3}, T.W{a4, a5, a6, a7}, T.W{a8, a9, a10, a11}, T.W{a12, a13, a14, a15}}:
47      {==}