def tr.mac

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

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

1200def 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}:
1201  %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}
1202  %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}
1203  %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}
1204  %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}
1205  %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}
1206  %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}
1207  {==}