def mask_eout

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

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

285# the ciphertext's bytes are bytes, and as many as the message's
286def mask_eout(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun) -> {G.ad.ae.eout(xs, sb, r) == B.mask(G.ad.ae.eout(xs, sb, r)) : List<&2, U32>}:
287  match xs:
288    case Nil{}:
289      {==}
290    case Con{+x, t}:
291      %byte_byte(U32.xor(x, G.ad.ae.zhead(r))) : {Con{B.byte(U32.xor(x, G.ad.ae.zhead(r))), G.ad.ae.eout(t, sb, G.ad.ae.step(sb, r, B.byte(x)))} == Con{_, B.mask(G.ad.ae.eout(t, sb, G.ad.ae.step(sb, r, B.byte(x))))} : List<&2, U32>}
292      %mask_eout(t, sb, G.ad.ae.step(sb, r, B.byte(x))) : {Con{B.byte(U32.xor(x, G.ad.ae.zhead(r))), G.ad.ae.eout(t, sb, G.ad.ae.step(sb, r, B.byte(x)))} == Con{B.byte(U32.xor(x, G.ad.ae.zhead(r))), _} : List<&2, U32>}
293      {==}