def open_checked

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/aes/gcm.bend:159

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/subtle.bend as Eq

159def open_checked(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +iv: List<&2, U32>, +aad: List<&2, U32>, +c: List<&2, U32>, t: List<&2, U32>) -> Maybe<&2, List<&2, U32>>:
160  accept(Eq.equal(t, tag(nk, nr, key, iv, aad, c)), gctr(nk, nr, key, c, inc32(j0(iv))))