law g_len

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aead/sound.bend:165

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

165law g_len:
166  for +short: Bool
167  for +nk: Nat
168  for +nr: Nat
169  for +key: List<&2, U32>
170  for +iv: List<&2, U32>
171  for +aad: List<&2, U32>
172  for +input: List<&2, U32>
173  for +p: List<&2, U32>
174  for +h: {G.open_split(nk, nr, key, iv, aad, input, List.length(&2, U32, input), short) == Some{p} : Maybe<&2, List<&2, U32>>}
175  {G.seal(nk, nr, key, iv, aad, p) == input : List<&2, U32>}