PROOF.aegis_rt: def of bend-osdev-aead@0.1.0.0
Import: import bend-osdev-aead@0.1.0.0/PROOF.bend as PROOF
Lines 368-384 of bend-osdev-aead@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&start_line=368&end_line=384

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

def aegis_rt(b: Bool, +kk: G.AdAegisKey, +n: B.Octets, +a: B.Octets, +p: B.Octets, e: {Nat.is_eq(B.Octets.len(n), 16n) == b : Bool}, e2: {Nat.is_eq(B.Octets.len(n), 16n) == b : Bool}) -> {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, G.AdAegis128.seal(kk, n, a, p), c => G.AdAegis128.open(kk, n, a, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, G.AdAegis128.seal(kk, n, a, p)) : Result<&2, &2, Cr.CrError, B.Octets>}:
  match b:
    case True{}:
      match kk:
        case G.AdAegisKey{+k, +sb}:
          %seal_ok(G.AdAegisKey{k, sb}, n, a, p, e) : {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, _, c => G.AdAegis128.open(G.AdAegisKey{k, sb}, n, a, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, _) : Result<&2, &2, Cr.CrError, B.Octets>}
          %open_ok(G.AdAegisKey{k, sb}, n, a, G.ad.ae.seal.go(G.AdAegisKey{k, sb}, n, a, p), e2) : {_ == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
          %seal_go_eq(k, sb, n, a, p) : {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, Ad.AdTag.split(16n, _), s => G.ad.ae.open.go(G.AdAegisKey{k, sb}, n, a, s)) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
          %Equal.sym(Nat, 16n, B.Octets.len(G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p))), fin_len(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p))) : {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, Ad.AdTag.split(_, B.Octets.append(B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p)))), s => G.ad.ae.open.go(G.AdAegisKey{k, sb}, n, a, s)) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
          %split_join(B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p))) : {Result.bind(&2, &2, Cr.CrError, Ad.AdSplit, B.Octets, _, s => G.ad.ae.open.go(G.AdAegisKey{k, sb}, n, a, s)) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
          %tag_of_eq(k, sb, n, a, p) : {G.ad.ae.check(Ad.AdTag.is_eq(_, G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p))), G.ad.ae.plain(G.AdAegisKey{k, sb}, n, a, B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))))) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
          %is_eq_refl(G.ad.ae.final(sb, G.ad.ae.flush(sb, G.ad.ae.eafter(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))), B.Octets.len(a), B.Octets.len(p))) : {G.ad.ae.check(_, G.ad.ae.plain(G.AdAegisKey{k, sb}, n, a, B.Octets.of_list(G.ad.ae.eout(B.Octets.to_list(p), sb, G.ad.ae.start(sb, k, n, a))))) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
          %plain_eq(k, sb, n, a, p) : {G.ad.ae.check(True{}, _) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
          {==}
    case False{}:
      %seal_bad(kk, n, a, p, e) : {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, _, c => G.AdAegis128.open(kk, n, a, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, _) : Result<&2, &2, Cr.CrError, B.Octets>}
      {==}

Uses (37):
  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=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=fin_len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=is_eq_refl
  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=plain_eq
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=seal_bad
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=seal_go_eq
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=seal_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/PROOF.bend&name=tag_of_eq
  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.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-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.eafter
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.eout
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.final
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.flush
  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-aead@0.1.0.0/aegis128.bend&name=ad.ae.seal.go
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aegis128.bend&name=ad.ae.start
  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-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.to_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/crypto.bend&name=CrError