def auth_from_checked_hash

qasim-bend-kit@0.1.0.2 · proof/AES_NistTagProof.bend:25

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

25def auth_from_checked_hash(+words: List<&2, U32>, +h: List<&2, U32>,
26    +aad: List<&2, U32>, +bytes: List<&2, U32>, +auth: List<&2, U32>,
27    hash_matches: {Core.aes256_encrypt_expanded(words, [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]) == h : List<&2, U32>},
28    computed: {auth_from_hash(h, aad, bytes) == auth : List<&2, U32>}) ->
29    {Core.ghash_auth_expanded(words, aad, bytes) == auth : List<&2, U32>}:
30    Equal.trans(List<&2, U32>,
31        Core.ghash_auth_expanded(words, aad, bytes),
32        auth_from_hash(h, aad, bytes), auth,
33        Equal.cong(List<&2, U32>, List<&2, U32>, h => auth_from_hash(h, aad, bytes),
34            Core.aes256_encrypt_expanded(words, [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]), h, hash_matches),
35        computed)