LAWS.aegis128_round_trip: law of bend-osdev-aead@0.1.0.0
Import: import bend-osdev-aead@0.1.0.0/LAWS.bend as LAWS
Lines 34-39 of bend-osdev-aead@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-aead@0.1.0.0/LAWS.bend&start_line=34&end_line=39

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

law aegis128_round_trip:
  for +k: G.AdAegisKey
  for +n: B.Octets
  for +a: B.Octets
  for +p: B.Octets
  {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>}

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.bind
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.map
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=aegis_rt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=AdAegis128.open
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=AdAegis128.seal
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=AdAegisKey
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/crypto.bend&name=CrError