PROOF.tr.aad: def of bend-osdev-cipher-modes@0.1.0.0
Import: import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF
Lines 1191-1198 of bend-osdev-cipher-modes@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&start_line=1191&end_line=1198

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

def tr.aad(empty: Bool, +a: List<&2, U32>) -> {CC.ccm.aad.pick(empty, a) == CC.ccm.aad.pick.fast(empty, a) : List<&2, U32>}:
  match empty:
    case True{}:
      {==}
    case False{}:
      %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>}
      %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>}
      {==}

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=len_fast
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.pad
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.aad.pick
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.aad.pick.fast
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.alen.pick
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.pad.fast