def open_split

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

import Base

162# GCM-AD_K(IV, C, A, T), the input being C || T: FAIL (None) unless T is
163# the tag of C.
164def open_split(+nk: Nat, +nr: Nat, +key: List<&2, U32>, +iv: List<&2, U32>, +aad: List<&2, U32>, +input: List<&2, U32>, +n: Nat, short: Bool) -> Maybe<&2, List<&2, U32>>:
165  match short:
166    case True{}:
167      None{}
168    case False{}:
169      open_checked(nk, nr, key, iv, aad, List.take(&2, U32, input, Nat.sub(n, 16n)), List.drop(&2, U32, input, Nat.sub(n, 16n)))