~/jendhub

def dec_enc_after

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

import bend-osdev-aead@0.1.0.0/PROOF.bend as PROOF
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

266# decryption runs through the states encryption ran through, and gives the
267# message's bytes back
268def dec_enc_after(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun) -> {G.ad.ae.eafter(xs, sb, r) == G.ad.ae.dafter(G.ad.ae.eout(xs, sb, r), sb, r) : G.AdAegisRun}:
269  match xs:
270    case Nil{}:
271      {==}
272    case Con{+x, t}:
273      %byte_xx(x, G.ad.ae.zhead(r)) : {G.ad.ae.eafter(t, sb, G.ad.ae.step(sb, r, B.byte(x))) == G.ad.ae.dafter(G.ad.ae.eout(t, sb, G.ad.ae.step(sb, r, B.byte(x))), sb, G.ad.ae.step(sb, r, _)) : G.AdAegisRun}
274      dec_enc_after(t, sb, G.ad.ae.step(sb, r, B.byte(x)))

Uses (11)

Used by (1)