~/jendhub

def checkpoint_nist_schedule

qasim-bend-kit@0.1.0.2 · proof/AES_NistVectorProof.bend:12

import qasim-bend-kit@0.1.0.2/proof/AES_NistVectorProof.bend as AESNistVectorProof
import Base
import qasim-bend-kit@0.1.0.2/LAWS.bend as L
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
import qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend as Key
import qasim-bend-kit@0.1.0.2/proof/AES_NistObservationProof.bend as Obs

12def checkpoint_nist_schedule() ->
13    {Core.aes256_expand(AES.secret_key_bytes(L.aes256gcm_nist_key())) == Key.words_60() : List<&2, U32>}:
14    Obs.schedule_input_matches(L.aes256gcm_nist_key(), Key.key_bytes(), Key.words_60(), {==}, Key.key_schedule_matches())

Uses (9)

Used by (13)