PROOF.tr.mac: 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 1200-1207 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=1200&end_line=1207

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/cipher_modes.bend as M
import bend-osdev-cipher-modes@0.1.0.0/ccm.bend as CC

def tr.mac(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +l: Nat, +nonce: List<&2, U32>, +a: List<&2, U32>, +p: List<&2, U32>) -> {CC.ccm.mac(~K, ~enc, k, m, l, nonce, a, p) == CC.ccm.mac.fast(~K, ~enc, k, m, l, nonce, a, p) : M.CmBlock}:
  %BL.len_fast(a) : {CC.ccm.mac(~K, ~enc, k, m, l, nonce, a, p) == CC.ccm.cbcmac(~K, ~enc, k, M.cm.split.blocks(M.cm.split.fast(B.append(Con{U32.from_nat(Nat.add(Nat.add(Nat.mul(64n, Nat.min(_, 1n)), Nat.mul(8n, Nat.div(Nat.sub(m, 2n), 2n))), Nat.sub(l, 1n))), B.append(nonce, CC.ccm.be(l, U32.from_nat(B.len.fast(p))))}, B.append.fast(CC.ccm.aad.pick.fast(Nat.is_eq(_, 0n), a), CC.ccm.pad.fast(p))))), M.CmBlock.zero()) : M.CmBlock}
  %BL.len_fast(p) : {CC.ccm.mac(~K, ~enc, k, m, l, nonce, a, p) == CC.ccm.cbcmac(~K, ~enc, k, M.cm.split.blocks(M.cm.split.fast(B.append(Con{U32.from_nat(Nat.add(Nat.add(Nat.mul(64n, Nat.min(B.len(a), 1n)), Nat.mul(8n, Nat.div(Nat.sub(m, 2n), 2n))), Nat.sub(l, 1n))), B.append(nonce, CC.ccm.be(l, U32.from_nat(_)))}, B.append.fast(CC.ccm.aad.pick.fast(Nat.is_eq(B.len(a), 0n), a), CC.ccm.pad.fast(p))))), M.CmBlock.zero()) : M.CmBlock}
  %tr.pad(p) : {CC.ccm.mac(~K, ~enc, k, m, l, nonce, a, p) == CC.ccm.cbcmac(~K, ~enc, k, M.cm.split.blocks(M.cm.split.fast(B.append(Con{U32.from_nat(Nat.add(Nat.add(Nat.mul(64n, Nat.min(B.len(a), 1n)), Nat.mul(8n, Nat.div(Nat.sub(m, 2n), 2n))), Nat.sub(l, 1n))), B.append(nonce, CC.ccm.be(l, U32.from_nat(B.len(p))))}, B.append.fast(CC.ccm.aad.pick.fast(Nat.is_eq(B.len(a), 0n), a), _)))), M.CmBlock.zero()) : M.CmBlock}
  %tr.aad(Nat.is_eq(B.len(a), 0n), a) : {CC.ccm.mac(~K, ~enc, k, m, l, nonce, a, p) == CC.ccm.cbcmac(~K, ~enc, k, M.cm.split.blocks(M.cm.split.fast(B.append(Con{U32.from_nat(Nat.add(Nat.add(Nat.mul(64n, Nat.min(B.len(a), 1n)), Nat.mul(8n, Nat.div(Nat.sub(m, 2n), 2n))), Nat.sub(l, 1n))), B.append(nonce, CC.ccm.be(l, U32.from_nat(B.len(p))))}, B.append.fast(_, CC.ccm.pad(p))))), M.CmBlock.zero()) : M.CmBlock}
  %BL.append_fast(CC.ccm.aad.pick(Nat.is_eq(B.len(a), 0n), a), CC.ccm.pad(p)) : {CC.ccm.mac(~K, ~enc, k, m, l, nonce, a, p) == CC.ccm.cbcmac(~K, ~enc, k, M.cm.split.blocks(M.cm.split.fast(B.append(Con{U32.from_nat(Nat.add(Nat.add(Nat.mul(64n, Nat.min(B.len(a), 1n)), Nat.mul(8n, Nat.div(Nat.sub(m, 2n), 2n))), Nat.sub(l, 1n))), B.append(nonce, CC.ccm.be(l, U32.from_nat(B.len(p))))}, _))), M.CmBlock.zero()) : M.CmBlock}
  %tr.split_eq(B.append(Con{U32.from_nat(Nat.add(Nat.add(Nat.mul(64n, Nat.min(B.len(a), 1n)), Nat.mul(8n, Nat.div(Nat.sub(m, 2n), 2n))), Nat.sub(l, 1n))), B.append(nonce, CC.ccm.be(l, U32.from_nat(B.len(p))))}, B.append(CC.ccm.aad.pick(Nat.is_eq(B.len(a), 0n), a), CC.ccm.pad(p)))) : {CC.ccm.mac(~K, ~enc, k, m, l, nonce, a, p) == CC.ccm.cbcmac(~K, ~enc, k, M.cm.split.blocks(_), M.CmBlock.zero()) : M.CmBlock}
  {==}

Uses (31):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.min
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  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=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=append_fast
  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=append.fast
  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-bytes@0.1.1.0/bytes.bend&name=len.fast
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.aad
  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/PROOF.bend&name=tr.split_eq
  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.be
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.cbcmac
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.mac
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.mac.fast
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.pad
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.pad.fast
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=CmBlock
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=CmBlock.zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=cm.split.blocks
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=cm.split.fast