def ego_ref

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

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-aead@0.1.0.0/aesround.bend as R
import bend-osdev-aead@0.1.0.0/aegis128.bend as G

252def ego_ref(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun, +acc: List<&2, U32>) -> {G.AdAegisOut{G.ad.ae.eafter(xs, sb, r), G.ad.ae.rev(acc, G.ad.ae.eout(xs, sb, r))} == G.ad.ae.ego(xs, sb, r, acc) : G.AdAegisOut}:
253  match xs:
254    case Nil{}:
255      {==}
256    case Con{+x, t}:
257      ego_ref(t, sb, G.ad.ae.step(sb, r, B.byte(x)), Con{B.byte(U32.xor(x, G.ad.ae.zhead(r))), acc})