def aegis_rt

bend-osdev-aead@0.1.0.0 · PROOF.bend:368

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

368def 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>}:
369  match b:
370    case True{}:
371      match kk:
372        case G.AdAegisKey{+k, +sb}:
373          %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>}
374          %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>}
375          %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>}
376          %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>}
377          %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>}
378          %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>}
379          %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>}
380          %plain_eq(k, sb, n, a, p) : {G.ad.ae.check(True{}, _) == Done{p} : Result<&2, &2, Cr.CrError, B.Octets>}
381          {==}
382    case False{}:
383      %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>}
384      {==}