def len_eout

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

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

295def len_eout(xs: List<&2, U32>, +sb: R.AdSbox, +r: G.AdAegisRun) -> {B.len(xs) == B.len(G.ad.ae.eout(xs, sb, r)) : Nat}:
296  match xs:
297    case Nil{}:
298      {==}
299    case Con{+x, t}:
300      %len_eout(t, sb, G.ad.ae.step(sb, r, B.byte(x))) : {1n+B.len(t) == 1n+_ : Nat}
301      {==}