AESNistObservationProof.schedule_input_matches: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend as AESNistObservationProof
Lines 10-16 of qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend&start_line=10&end_line=16

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

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

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=SecretKey
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=secret_key_bytes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend&name=aes256_expand