def key_schedule_matches

qasim-bend-kit@0.1.0.2 · proof/AES_NistKeyScheduleProof.bend:958

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
import qasim-bend-kit@0.1.0.2/proof/AES_TraceBridgeProof.bend as Bridge

958def key_schedule_matches() ->
959    {Core.aes256_expand(key_bytes()) == words_60() : List<&2, U32>}:
960    Bridge.public_expansion_matches(key_bytes(), words_60(),
961        Bridge.expand_key_matches(52n, key_bytes(), words_8(), words_60(),
962            {==}, expanded_words_matches()))