def dgo_ref

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

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

259def dgo_ref(ys: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun, +acc: List<&2, U32>) -> {G.AdAegisOut{G.ad.ae.dafter(ys, sb, r), G.ad.ae.rev(acc, G.ad.ae.dout(ys, sb, r))} == G.ad.ae.dgo(ys, sb, r, acc) : G.AdAegisOut}:
260  match ys:
261    case Nil{}:
262      {==}
263    case Con{+y, t}:
264      dgo_ref(t, sb, G.ad.ae.step(sb, r, B.byte(U32.xor(y, G.ad.ae.zhead(r)))), Con{B.byte(U32.xor(y, G.ad.ae.zhead(r))), acc})