def tb

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/aead.bend:383

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G

383def tb(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +iv: List<&2, U32>, +aad: List<&2, U32>, +c: List<&2, U32>, +i: Nat) -> U32:
384  U32.xor(S.nth_byte(hb(nk, nr, key, aad, c), i), kb(nk, nr, key, G.j0(iv), i))