PROOF.ccmp.main: 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 1850-1892 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=1850&end_line=1892

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

# decryption accepts what encryption produced, whatever the parameter checks answer
def ccmp.main(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +m: Nat, +nonce: B.Octets, +aad: B.Octets, +p: B.Octets, r: Result<&2, &2, M.CmError, Unit>) -> {CC.ccm.checks(m, B.len(B.Octets.to_list(nonce)), B.len(B.Octets.to_list(p))) == r : Result<&2, &2, M.CmError, Unit>} -> {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, CC.ccm.e2(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p), r), c => CC.Ccm.decrypt.ref(~K, ~enc, k, m, nonce, aad, c)) == Result.map(&2, &2, M.CmError, B.Octets, B.Octets, c => p, CC.ccm.e2(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p), r)) : Result<&2, &2, M.CmError, B.Octets>}:
  match r:
    case Fail{e}:
      h => {==}
    case Done{+u}:
      +h => +hm = ccmp.tag_le(m, B.len(B.Octets.to_list(nonce)), B.len(B.Octets.to_list(p)), u, h)
        +leb = ccmp.len_eb(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p), hm)
        # decryption reads the ciphertext back, masked
        %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))))), B.mask(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), BL.octets_to_of(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))))) : {CC.ccm.d2(~K, ~enc, Nat.is_le(m, B.len(_)), k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), _) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # which it already is
        %Equal.sym(List<&2, U32>, B.mask(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))), ccmp.mask_eb(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))) : {CC.ccm.d2(~K, ~enc, Nat.is_le(m, B.len(_)), k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), _) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # it is longer than the tag
        %Equal.sym(Nat, B.len(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), Nat.add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m), leb) : {CC.ccm.d2(~K, ~enc, Nat.is_le(m, _), k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # 
        %Equal.sym(Bool, Nat.is_le(m, Nat.add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m)), True{}, na.le_add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m)) : {CC.ccm.d2(~K, ~enc, _, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # its body is as long as the message
        %Equal.sym(Nat, B.len(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), Nat.add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m), leb) : {CC.ccm.d3(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))), CC.ccm.checks(m, B.len(B.Octets.to_list(nonce)), Nat.sub(_, m))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # 
        %Equal.sym(Nat, Nat.sub(Nat.add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m), m), B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), na.sub_add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m)) : {CC.ccm.d3(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))), CC.ccm.checks(m, B.len(B.Octets.to_list(nonce)), _)) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # 
        %Equal.sym(Nat, B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), B.len(B.Octets.to_list(p)), ccmp.len_xcp(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), p)) : {CC.ccm.d3(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))), CC.ccm.checks(m, B.len(B.Octets.to_list(nonce)), _)) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # so its checks pass as encryption's did
        %Equal.sym(Result<&2, &2, M.CmError, Unit>, CC.ccm.checks(m, B.len(B.Octets.to_list(nonce)), B.len(B.Octets.to_list(p))), Done{u}, h) : {CC.ccm.d3(~K, ~enc, k, m, B.Octets.to_list(nonce), B.Octets.to_list(aad), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))), _) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # the body and the tag apart
        %Equal.sym(Nat, B.len(B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), Nat.add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m), leb) : {CC.ccm.open(M.cm.ct_eq(M.cm.xor_bytes(B.drop(Nat.sub(_, m), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.take(Nat.sub(_, m), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))))))), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.take(Nat.sub(_, m), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))))))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # 
        %Equal.sym(Nat, Nat.sub(Nat.add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m), m), B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), na.sub_add(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), m)) : {CC.ccm.open(M.cm.ct_eq(M.cm.xor_bytes(B.drop(_, B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.take(_, B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))))))), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.take(_, B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))))))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # 
        %Equal.sym(List<&2, U32>, B.take(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), li.take_append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))) : {CC.ccm.open(M.cm.ct_eq(M.cm.xor_bytes(B.drop(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(_)))), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(_))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # 
        %Equal.sym(List<&2, U32>, B.drop(B.len(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))), B.append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), li.drop_append(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))), M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))))) : {CC.ccm.open(M.cm.ct_eq(M.cm.xor_bytes(_, M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))))))), CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p)))))) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # CTR undoes itself: the plaintext
        %Equal.sym(List<&2, U32>, CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(CC.ccm.xcrypt(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), M.cm.split(B.Octets.to_list(p))))), B.Octets.to_list(p), ccmp.xxp(~K, ~enc, k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)), p)) : {CC.ccm.open(M.cm.ct_eq(M.cm.xor_bytes(M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), _)), _) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # the received tag, unmasked from S_0
        %Equal.sym(List<&2, U32>, M.cm.xor_bytes(M.cm.xor_bytes(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce))))), B.mask(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))), li.xor_xor(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), M.cm.bytes_of(enc(k, CC.ccm.a0(Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce)))))(ccmp.le_tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p), hm))) : {CC.ccm.open(M.cm.ct_eq(_, CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))), B.Octets.to_list(p)) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # 
        %Equal.sym(List<&2, U32>, B.mask(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), ccmp.mask_tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))) : {CC.ccm.open(M.cm.ct_eq(_, CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))), B.Octets.to_list(p)) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # matches the tag recomputed
        %Equal.sym(Bool, M.cm.ct_eq(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)), CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p))), True{}, ccmp.ct_refl(CC.ccm.tag(~K, ~enc, k, m, Nat.sub(15n, B.len(B.Octets.to_list(nonce))), B.Octets.to_list(nonce), B.Octets.to_list(aad), B.Octets.to_list(p)))) : {CC.ccm.open(_, B.Octets.to_list(p)) == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        # 
        %Equal.sym(B.Octets, B.Octets.of_list(B.Octets.to_list(p)), p, BL.octets_of_to(p)) : {Done{_} == Done{p} : Result<&2, &2, M.CmError, B.Octets>}
        {==}

Uses (50):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.bind
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.map
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_of_to
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_to_of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.to_list
  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=drop
  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=mask
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=take
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=ccmp.ct_refl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=ccmp.le_tag
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=ccmp.len_eb
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=ccmp.len_xcp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=ccmp.mask_eb
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=ccmp.mask_tag
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=ccmp.tag_le
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=ccmp.xxp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.drop_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.take_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.xor_xor
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=na.le_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=na.sub_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=Ccm.decrypt.ref
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.a0
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.checks
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.d2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.d3
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.e2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.open
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.tag
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/ccm.bend&name=ccm.xcrypt
  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=CmError
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=cm.bytes_of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=cm.ct_eq
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=cm.split
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=cm.xor_bytes