def schedule_input_matches

qasim-bend-kit@0.1.0.2 · proof/AES_NistObservationProof.bend:10

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

10def schedule_input_matches(+key: AES.SecretKey, +bytes: List<&2, U32>, +words: List<&2, U32>,
11    input_matches: {AES.secret_key_bytes(key) == bytes : List<&2, U32>},
12    computed: {Core.aes256_expand(bytes) == words : List<&2, U32>}) ->
13    {Core.aes256_expand(AES.secret_key_bytes(key)) == words : List<&2, U32>}:
14    Equal.trans(List<&2, U32>, Core.aes256_expand(AES.secret_key_bytes(key)), Core.aes256_expand(bytes), words,
15        Equal.cong(List<&2, U32>, List<&2, U32>, value => Core.aes256_expand(value),
16            AES.secret_key_bytes(key), bytes, input_matches), computed)