law aegis128_round_trip

bend-osdev-aead@0.1.0.0 · LAWS.bend:34

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
import bend-osdev-aead@0.1.0.0/aegis128.bend as G

34law aegis128_round_trip:
35  for +k: G.AdAegisKey
36  for +n: B.Octets
37  for +a: B.Octets
38  for +p: B.Octets
39  {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, G.AdAegis128.seal(k, n, a, p), c => G.AdAegis128.open(k, n, a, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, G.AdAegis128.seal(k, n, a, p)) : Result<&2, &2, Cr.CrError, B.Octets>}