~/jendhub

def tag_len

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

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

317def tag_len(st: G.AdAegisSt) -> {16n == B.Octets.len(G.ad.ae.tag(st)) : Nat}:
318  match st:
319    case G.AdAegisSt{a0, a1, a2, a3, a4}:
320      blk_len(R.AdBlk.xor(R.AdBlk.xor(R.AdBlk.xor(a0, a1), R.AdBlk.xor(a2, a3)), a4))

Uses (6)

Used by (1)