def ad.ae.step

bend-osdev-aead@0.1.0.0 · aegis128.bend:114

import Base
import bend-osdev-aead@0.1.0.0/aesround.bend as R

114# the run after the plaintext byte x
115def ad.ae.step(+sb: R.AdSbox, r: AdAegisRun, x: U32) -> AdAegisRun:
116  match r:
117    case AdAegisRun{st, zs, buf, +n}:
118      ad.ae.step.pick(Nat.is_eq(n, 15n), sb, st, zs, Con{x, buf}, n)