LAWS.aegis128_tamper: law of bend-osdev-aead@0.1.0.0
Import: import bend-osdev-aead@0.1.0.0/LAWS.bend as LAWS
Lines 41-52 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=41&end_line=52

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/aead.bend as Ad
import bend-osdev-aead@0.1.0.0/aegis128.bend as G

# a tag of 16 bytes other than the one AEGIS-128 computes for the ciphertext
# is refused, under a 16-byte nonce
law aegis128_tamper:
  for +k: G.AdAegisKey
  for +n: B.Octets
  for +a: B.Octets
  for +c: B.Octets
  for +t: B.Octets
  for hn: {B.Octets.len(n) == 16n : Nat}
  for hl: {B.Octets.len(t) == 16n : Nat}
  for ht: {Ad.AdTag.is_eq(G.AdAegis128.tag_of(k, n, a, c), t) == False{} : Bool}
  {G.AdAegis128.open(k, n, a, B.Octets.append(c, t)) == Fail{Cr.CrTagMismatch{}} : Result<&2, &2, Cr.CrError, B.Octets>}

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=bend-osdev-aead@0.1.0.0/PROOF.bend&name=nonce_ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=open_ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=split_join
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aead.bend&name=AdSplit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aead.bend&name=AdTag.is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aead.bend&name=AdTag.split
  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.tag_of
  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-aead@0.1.0.0/aegis128.bend&name=ad.ae.check
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.open.go
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.plain
  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.append
  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