def tr.aad

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1191

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL
import bend-osdev-cipher-modes@0.1.0.0/ccm.bend as CC

1191def tr.aad(empty: Bool, +a: List<&2, U32>) -> {CC.ccm.aad.pick(empty, a) == CC.ccm.aad.pick.fast(empty, a) : List<&2, U32>}:
1192  match empty:
1193    case True{}:
1194      {==}
1195    case False{}:
1196      %BL.len_fast(a) : {CC.ccm.aad.pick(False{}, a) == CC.ccm.pad.fast(B.append(CC.ccm.alen.pick(U32.is_lt(U32.from_nat(_), 65280), U32.from_nat(_)), a)) : List<&2, U32>}
1197      %tr.pad(B.append(CC.ccm.alen.pick(U32.is_lt(U32.from_nat(B.len(a)), 65280), U32.from_nat(B.len(a))), a)) : {CC.ccm.aad.pick(False{}, a) == _ : List<&2, U32>}
1198      {==}