bend-osdev-cipher-modes

Releases (1):
  0.1.0.0  0xf4b936e0e6b2608080d2f02bb3ce9abe  indexed  https://jend.leeeet.dev/files.txt?path=bend-osdev-cipher-modes@0.1.0.0

Definitions (444, 1 to 100 shown):
  LAWS.cbc_blocks_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=cbc_blocks_round_trip)
   # CBC on blocks: decryption undoes encryption, for every key, IV and message
   law cbc_blocks_round_trip:
     for ~K: Data
     for ~enc: K -> M.CmBlock -> M.CmBlock
     for ~dec: K -> M.CmBlock -> M.CmBlock
     for ~inv: @k: K -> @b: M.CmBlock -> {dec(k, enc(k, b)) == b : M.CmBlock}
     for +k: K
     for iv: M.CmBlock
     for bs: List<&2, M.CmBlock>
     {C.Cbc.decrypt_blocks(~K, ~dec, k, iv, C.Cbc.encrypt_blocks(~K, ~enc, k, iv, bs)) == bs : List<&2, M.CmBlock>}
  LAWS.cbc_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=cbc_round_trip)
   # CBC on bytes: for every 16-byte IV and every message of whole blocks,
   # encryption succeeds and decryption gives the message back
   law cbc_round_trip:
     for ~K: Data
     for ~enc: K -> M.CmBlock -> M.CmBlock
     for ~dec: K -> M.CmBlock -> M.CmBlock
     for ~inv: @k: K -> @b: M.CmBlock -> {dec(k, enc(k, b)) == b : M.CmBlock}
     for +k: K
     for +iv: B.Octets
     for +m: B.Octets
     for hi: {B.Octets.len(iv) == 16n : Nat}
     …
  LAWS.xts_blocks_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=xts_blocks_round_trip)
   # XTS on blocks: decryption undoes encryption, for every data key and every
   # starting tweak (T_0 = Xts.tweak(k2, i), so every k2 and i are covered)
   law xts_blocks_round_trip:
     for ~K: Data
     for ~enc: K -> M.CmBlock -> M.CmBlock
     for ~dec: K -> M.CmBlock -> M.CmBlock
     for ~inv: @k: K -> @b: M.CmBlock -> {dec(k, enc(k, b)) == b : M.CmBlock}
     for +k1: K
     for t: M.CmBlock
     for bs: List<&2, M.CmBlock>
     {T.Xts.decrypt_blocks(~K, ~dec, k1, t, T.Xts.encrypt_blocks(~K, ~enc, k1, t, bs)) == bs : List<&2, M.CmBlock>}
  LAWS.cmac_streaming (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=cmac_streaming)
   # CMAC in pieces: the state after a ++ b is the state after a, then b, for
   # every cipher, key and state (so start, update .. update, finish is the MAC
   # of the pieces joined)
   law cmac_streaming:
     for ~K: Data
     for ~enc: K -> M.CmBlock -> M.CmBlock
     for +k: K
     for s: CM.CmacState
     for +a: B.Octets
     for +b: B.Octets
     {CM.Cmac.update(~K, ~enc, k, s, B.Octets.append(a, b)) == CM.Cmac.update(~K, ~enc, k, CM.Cmac.update(~K, ~enc, k, s, a), b) : CM.CmacState}
  LAWS.xts_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=xts_round_trip)
   # XTS on bytes, with ciphertext stealing: for every 16-byte sequence number
   # and every data unit of at least 16 bytes, encryption succeeds and
   # decryption gives the data unit back
   law xts_round_trip:
     for ~K: Data
     for ~enc: K -> M.CmBlock -> M.CmBlock
     for ~dec: K -> M.CmBlock -> M.CmBlock
     for ~inv: @k: K -> @b: M.CmBlock -> {dec(k, enc(k, b)) == b : M.CmBlock}
     for +k1: K
     for +k2: K
     for +i: B.Octets
     …
  LAWS.ccm_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=ccm_round_trip)
   # CCM: decryption accepts what encryption produced and gives the message
   # back, for every cipher, key, tag length, nonce, associated data and
   # message; when the parameters are refused, both refuse alike
   law ccm_round_trip:
     for ~K: Data
     for ~enc: K -> M.CmBlock -> M.CmBlock
     for +k: K
     for +m: Nat
     for +nonce: B.Octets
     for +aad: B.Octets
     for +p: B.Octets
     {Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, CC.Ccm.encrypt(~K, ~enc, k, m, nonce, aad, p), c => CC.Ccm.decrypt(~K, ~enc, k, m, nonce, aad, c)) == Result.map(&2, &2, M.CmError, B.Octets, B.Octets, c => p, CC.Ccm.encrypt(~K, ~enc, k, m, nonce, aad, p)) : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.block_octets_round_trip (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=block_octets_round_trip)
   # A block written as Octets reads back as the same block, for every block
   law block_octets_round_trip:
     for +b: M.CmBlock
     {M.CmBlock.of_octets(M.CmBlock.to_octets(b)) == Some{b} : Maybe<&2, M.CmBlock>}
  LAWS.aes128_fips197_c1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=aes128_fips197_c1)
   # FIPS 197 Appendix C.1: the named default cipher (AES-128) encrypts one block
   law aes128_fips197_c1:
     {Result.map(&2, &2, M.CmError, X.CmAesKey, B.Octets, k => M.CmBlock.to_octets(X.CmAes.encrypt(k, M.CmBlock{1122867, 1146447479, 2291772091, 3437096703})), X.CmAes.key128(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]))) == Done{B.Octets.of_list([105, 196, 224, 216, 106, 123, 4, 48, 216, 205, 183, 128, 112, 180, 197, 90])} : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.aes_bad_key_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=aes_bad_key_length)
   # a key of a length AES-128 and AES-256 do not have is refused
   law aes_bad_key_length:
     {D.CmAes.cbc_encrypt(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42])) == Fail{M.CmBadKeyLength{15n}} : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.cbc_sp800_38a_f21_block1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=cbc_sp800_38a_f21_block1)
   # NIST SP 800-38A Appendix F.2.1, CBC-AES128: its first block
   law cbc_sp800_38a_f21_block1:
     {D.CmAes.cbc_encrypt(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42])) == Done{B.Octets.of_list([118, 73, 171, 172, 129, 25, 178, 70, 206, 233, 142, 155, 18, 233, 25, 125])} : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.cbc_not_whole_blocks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=cbc_not_whole_blocks)
   # the byte layer refuses a message that is not whole blocks, and a short IV
   law cbc_not_whole_blocks:
     {D.CmAes.cbc_encrypt(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42, 174])) == Fail{M.CmNotBlockMultiple{17n}} : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.cbc_short_iv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=cbc_short_iv)
   law cbc_short_iv:
     {D.CmAes.cbc_encrypt(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14]), B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42])) == Fail{M.CmBadIvLength{15n}} : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.pkcs7_pad_empty (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=pkcs7_pad_empty)
   # PKCS #7 (RFC 5652, 6.3): the empty message becomes a whole block of 16s; 15 bytes gain one 1
   law pkcs7_pad_empty:
     {P.Pkcs7.pad(16n, B.Octets.empty()) == Done{B.Octets.of_list([16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16])} : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.pkcs7_pad_15 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=pkcs7_pad_15)
   law pkcs7_pad_15:
     {P.Pkcs7.pad(16n, B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23])) == Done{B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 1])} : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.pkcs7_unpad_15 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=pkcs7_unpad_15)
   law pkcs7_unpad_15:
     {P.Pkcs7.unpad(16n, B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 1])) == Done{B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23])} : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.pkcs7_unpad_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=pkcs7_unpad_zero)
   # a last byte of 0, or one the bytes before it contradict, is bad padding
   law pkcs7_unpad_zero:
     {P.Pkcs7.unpad(16n, B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 0])) == Fail{M.CmBadPadding{}} : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.pkcs7_unpad_mixed (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=pkcs7_unpad_mixed)
   law pkcs7_unpad_mixed:
     {P.Pkcs7.unpad(16n, B.Octets.of_list([107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 2, 3, 3])) == Fail{M.CmBadPadding{}} : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.xts_short (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=xts_short)
   # a data unit shorter than a block is refused
   law xts_short:
     {D.CmAes.xts_encrypt(B.Octets.of_list([255, 254, 253, 252, 251, 250, 249, 248, 247, 246, 245, 244, 243, 242, 241, 240, 191, 190, 189, 188, 187, 186, 185, 184, 183, 182, 181, 180, 179, 178, 177, 176]), B.Octets.of_list([154, 120, 86, 52, 18, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]), B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0])) == Fail{M.CmTooShort{15n}} : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.xts_sector (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=xts_sector)
   # the sequence number of sector n: n little-endian, zero-filled to 16 bytes
   law xts_sector:
     {T.Xts.sector(W.W64.from_parts(0, 2591577138)) == B.Octets.of_list([50, 84, 120, 154, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) : B.Octets}
  LAWS.ccm_bad_tag_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=ccm_bad_tag_length)
   # a tag of odd length, and a nonce of 6 bytes, are refused
   law ccm_bad_tag_length:
     {D.CmAes.ccm_encrypt(B.Octets.of_list([192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207]), 7n, B.Octets.of_list([0, 0, 0, 3, 2, 1, 0, 160, 161, 162, 163, 164, 165]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7]), B.Octets.of_list([8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30])) == Fail{M.CmBadTagLength{7n}} : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.ccm_bad_nonce_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=ccm_bad_nonce_length)
   law ccm_bad_nonce_length:
     {D.CmAes.ccm_encrypt(B.Octets.of_list([192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 207]), 8n, B.Octets.of_list([0, 0, 0, 3, 2, 1]), B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7]), B.Octets.of_list([8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30])) == Fail{M.CmBadNonceLength{6n}} : Result<&2, &2, M.CmError, B.Octets>}
  LAWS.cmac_rfc4493_k1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/LAWS.bend&name=cmac_rfc4493_k1)
   # RFC 4493 section 4: the AES-CMAC subkey K1
   law cmac_rfc4493_k1:
     {Result.map(&2, &2, M.CmError, X.CmAesKey, B.Octets, k => M.CmBlock.to_octets(CM.Cmac.subkey1(~X.CmAesKey, ~X.CmAes.encrypt, k)), X.CmAes.key128(B.Octets.of_list([43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]))) == Done{B.Octets.of_list([251, 238, 214, 24, 53, 113, 51, 102, 124, 133, 224, 143, 114, 54, 168, 222])} : Result<&2, &2, M.CmError, B.Octets>}
  PROOF.bx.bool (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bx.bool)
   def bx.bool(a: Bool, b: Bool) -> {Bool.xor(a, Bool.xor(a, b)) == b : Bool}:
  PROOF.bx.word (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bx.word)
   def bx.word(n: Nat, a: Word(n), b: Word(n)) -> {Word.xor(n, a, Word.xor(n, a, b)) == b : Word(n)}:
  PROOF.bx.u32 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bx.u32)
   def bx.u32(a: U32, b: U32) -> {U32.xor(a, U32.xor(a, b)) == b : U32}:
  PROOF.bx.block (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bx.block)
   # xor(a, xor(a, b)) == b on blocks
   def bx.block(+a: M.CmBlock, +b: M.CmBlock) -> {M.CmBlock.xor(a, M.CmBlock.xor(a, b)) == b : M.CmBlock}:
  PROOF.bits.word_bytes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bits.word_bytes)
   def bits.word_bytes(w: U32) -> {M.cm.word(M.cm.b0(w), M.cm.b1(w), M.cm.b2(w), M.cm.b3(w)) == w : U32}:
  PROOF.bits.byte0_word (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bits.byte0_word)
   def bits.byte0_word(a: U32, b: U32, c: U32, d: U32) -> {M.cm.b0(M.cm.word(a, b, c, d)) == B.byte(a) : U32}:
  PROOF.bits.byte1_word (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bits.byte1_word)
   def bits.byte1_word(a: U32, b: U32, c: U32, d: U32) -> {M.cm.b1(M.cm.word(a, b, c, d)) == B.byte(b) : U32}:
  PROOF.bits.byte2_word (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bits.byte2_word)
   def bits.byte2_word(a: U32, b: U32, c: U32, d: U32) -> {M.cm.b2(M.cm.word(a, b, c, d)) == B.byte(c) : U32}:
  PROOF.bits.byte3_word (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bits.byte3_word)
   def bits.byte3_word(a: U32, b: U32, c: U32, d: U32) -> {M.cm.b3(M.cm.word(a, b, c, d)) == B.byte(d) : U32}:
  PROOF.bits.byte_b0 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bits.byte_b0)
   def bits.byte_b0(w: U32) -> {B.byte(M.cm.b0(w)) == M.cm.b0(w) : U32}:
  PROOF.bits.byte_b1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bits.byte_b1)
   def bits.byte_b1(w: U32) -> {B.byte(M.cm.b1(w)) == M.cm.b1(w) : U32}:
  PROOF.bits.byte_b2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bits.byte_b2)
   def bits.byte_b2(w: U32) -> {B.byte(M.cm.b2(w)) == M.cm.b2(w) : U32}:
  PROOF.bits.byte_b3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bits.byte_b3)
   def bits.byte_b3(w: U32) -> {B.byte(M.cm.b3(w)) == M.cm.b3(w) : U32}:
  PROOF.bits.byte_byte (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bits.byte_byte)
   def bits.byte_byte(y: U32) -> {B.byte(B.byte(y)) == B.byte(y) : U32}:
  PROOF.sp.cons_blocks (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.cons_blocks)
   def sp.cons_blocks(b: M.CmBlock, s: M.CmSplit) -> {M.cm.split.blocks(M.cm.split.cons(b, s)) == Con{b, M.cm.split.blocks(s)} : List<&2, M.CmBlock>}:
  PROOF.sp.cons_tail (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.cons_tail)
   def sp.cons_tail(b: M.CmBlock, s: M.CmSplit) -> {M.cm.split.tail(M.cm.split.cons(b, s)) == M.cm.split.tail(s) : List<&2, U32>}:
  PROOF.sp.eta (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.eta)
   def sp.eta(s: M.CmSplit) -> {M.CmSplit{M.cm.split.blocks(s), M.cm.split.tail(s)} == s : M.CmSplit}:
  PROOF.sp.disc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.disc)
   def sp.disc(n: Nat) -> Type:
  PROOF.sp.absurd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.absurd)
   def sp.absurd(p: Nat, h: {1n+p == 0n : Nat}) -> Empty:
  PROOF.sp.absurd_tail (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.absurd_tail)
   def sp.absurd_tail(p: Nat, xs: List<&2, U32>, h: {1n+p == 0n : Nat}) -> {M.cm.split.tail(M.cm.split(B.mask(xs))) == Nil{} : List<&2, U32>}:
  PROOF.sp.snd_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.snd_go)
   def sp.snd_go(n: Nat, m: Nat, d1: Nat, d2: Nat, r: Nat) -> {Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d1, r)) == Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d2, r)) : Nat}:
  PROOF.sp.mod16 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.mod16)
   def sp.mod16(n: Nat) -> {Nat.mod(Nat.add(16n, n), 16n) == Nat.mod(n, 16n) : Nat}:
  PROOF.bo.disc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bo.disc)
   def bo.disc(b: Bool) -> Type:
  PROOF.bo.empty (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bo.empty)
   def bo.empty(h: {False{} == True{} : Bool}) -> Empty:
  PROOF.bo.absurd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=bo.absurd)
   def bo.absurd(-A: Type, h: {False{} == True{} : Bool}) -> A:
  PROOF.li.mask_mask (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.mask_mask)
   def li.mask_mask(zs: List<&2, U32>) -> {B.mask(B.mask(zs)) == B.mask(zs) : List<&2, U32>}:
  PROOF.li.take_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.take_append)
   def li.take_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.take(B.len(a), B.append(a, b)) == a : List<&2, U32>}:
  PROOF.li.drop_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.drop_append)
   def li.drop_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.drop(B.len(a), B.append(a, b)) == b : List<&2, U32>}:
  PROOF.li.mask_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.mask_append)
   def li.mask_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.mask(B.append(a, b)) == B.append(B.mask(a), B.mask(b)) : List<&2, U32>}:
  PROOF.li.mask_drop (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.mask_drop)
   def li.mask_drop(+n: Nat, +xs: List<&2, U32>) -> {B.mask(B.drop(n, xs)) == B.drop(n, B.mask(xs)) : List<&2, U32>}:
  PROOF.li.mask_take (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.mask_take)
   def li.mask_take(+n: Nat, +xs: List<&2, U32>) -> {B.mask(B.take(n, xs)) == B.take(n, B.mask(xs)) : List<&2, U32>}:
  PROOF.li.len_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.len_append)
   def li.len_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.len(B.append(a, b)) == Nat.add(B.len(a), B.len(b)) : Nat}:
  PROOF.li.len_drop (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.len_drop)
   def li.len_drop(+n: Nat, +xs: List<&2, U32>) -> {B.len(B.drop(n, xs)) == Nat.sub(B.len(xs), n) : Nat}:
  PROOF.li.len_take (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=li.len_take)
   def li.len_take(+n: Nat, +xs: List<&2, U32>) -> {Nat.is_le(n, B.len(xs)) == True{} : Bool} -> {B.len(B.take(n, xs)) == n : Nat}:
  PROOF.na.add_sub (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=na.add_sub)
   def na.add_sub(+a: Nat, +b: Nat) -> {Nat.is_le(a, b) == True{} : Bool} -> {Nat.add(a, Nat.sub(b, a)) == b : Nat}:
  PROOF.na.lt_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=na.lt_le)
   def na.lt_le(+a: Nat, +b: Nat) -> {Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_le(a, b) == True{} : Bool}:
  PROOF.sp.hd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.hd)
   def sp.hd(bs: List<&2, M.CmBlock>) -> M.CmBlock:
  PROOF.sp.tl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.tl)
   def sp.tl(bs: List<&2, M.CmBlock>) -> List<&2, M.CmBlock>:
  PROOF.sp.blk (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.blk)
   # splitting the bytes of a block gives the block back
   def sp.blk(b: M.CmBlock, rest: List<&2, U32>) -> {M.cm.split(M.cm.bytes_onto(b, rest)) == M.cm.split.cons(b, M.cm.split(rest)) : M.CmSplit}:
  PROOF.sp.mask_blk (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.mask_blk)
   # the bytes of a block are bytes: masking changes nothing
   def sp.mask_blk(b: M.CmBlock, rest: List<&2, U32>) -> {B.mask(M.cm.bytes_onto(b, rest)) == M.cm.bytes_onto(b, B.mask(rest)) : List<&2, U32>}:
  PROOF.sp.blk16 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.blk16)
   # the block of 16 bytes, as bytes again
   def sp.blk16(y0: U32, y1: U32, y2: U32, y3: U32, y4: U32, y5: U32, y6: U32, y7: U32, y8: U32, y9: U32, y10: U32, y11: U32, y12: U32, y13: U32, y14: U32, y15: U32, rest: List<&2, U32>) -> {M.cm.bytes_onto(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), rest) == Con{B.byte(y0), Con{B.byte(y1), Con{B.byte(y2), Con{B.byte(y3), Con{B.byte(y4), Con{B.byte(y5), Con{B.byte(y6), Con{B.byte(y7), Con{B.byte(y8), Con{B.byte(y9), Con{B.byte(y10), Con{B.byte(y11), Con{B.byte(y12), Con{B.byte(y13), Con{B.byte(y14), Con{B.byte(y15), rest}}}}}}}}}}}}}}}} : List<&2, U32>}:
  PROOF.sp.join_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.join_split)
   # a masked list is its blocks and its tail joined back
   def sp.join_split(ys: List<&2, U32>) -> {M.cm.join_onto(M.cm.split.blocks(M.cm.split(B.mask(ys))), M.cm.split.tail(M.cm.split(B.mask(ys)))) == B.mask(ys) : List<&2, U32>}:
  PROOF.sp.mod_tail (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.mod_tail)
   # a list of whole blocks splits with no tail
   def sp.mod_tail(ys: List<&2, U32>) -> {Nat.mod(B.len(ys), 16n) == 0n : Nat} -> {M.cm.split.tail(M.cm.split(B.mask(ys))) == Nil{} : List<&2, U32>}:
  PROOF.sp.blk16g (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.blk16g)
   # the bytes of the block of any 16 values are those values, masked
   def sp.blk16g(z0: U32, z1: U32, z2: U32, z3: U32, z4: U32, z5: U32, z6: U32, z7: U32, z8: U32, z9: U32, z10: U32, z11: U32, z12: U32, z13: U32, z14: U32, z15: U32, rest: List<&2, U32>) -> {M.cm.bytes_onto(M.cm.block16(z0, z1, z2, z3, z4, z5, z6, z7, z8, z9, z10, z11, z12, z13, z14, z15), rest) == Con{B.byte(z0), Con{B.byte(z1), Con{B.byte(z2), Con{B.byte(z3), Con{B.byte(z4), Con{B.byte(z5), Con{B.byte(z6), Con{B.byte(z7), Con{B.byte(z8), Con{B.byte(z9), Con{B.byte(z10), Con{B.byte(z11), Con{B.byte(z12), Con{B.byte(z13), Con{B.byte(z14), Con{B.byte(z15), rest}}}}}}}}}}}}}}}} : List<&2, U32>}:
  PROOF.sp.tail_short (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.tail_short)
   # the tail of a split has fewer than 16 bytes
   def sp.tail_short(ys: List<&2, U32>) -> {Nat.is_lt(B.len(M.cm.split.tail(M.cm.split(B.mask(ys)))), 16n) == True{} : Bool}:
  PROOF.sp.tail_masked (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.tail_masked)
   # the tail of a masked split is masked
   def sp.tail_masked(ys: List<&2, U32>) -> {B.mask(M.cm.split.tail(M.cm.split(B.mask(ys)))) == M.cm.split.tail(M.cm.split(B.mask(ys))) : List<&2, U32>}:
  PROOF.sp.nonempty (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.nonempty)
   # a byte string of at least 16 bytes has a first block
   def sp.nonempty(ys: List<&2, U32>) -> {Nat.is_le(16n, B.len(ys)) == True{} : Bool} -> {Con{sp.hd(M.cm.split.blocks(M.cm.split(B.mask(ys)))), sp.tl(M.cm.split.blocks(M.cm.split(B.mask(ys))))} == M.cm.split.blocks(M.cm.split(B.mask(ys))) : List<&2, M.CmBlock>}:
  PROOF.sp.short_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.short_split)
   # fewer than 16 bytes are all tail
   def sp.short_split(ys: List<&2, U32>) -> {Nat.is_lt(B.len(ys), 16n) == True{} : Bool} -> {M.cm.split(ys) == M.CmSplit{Nil{}, ys} : M.CmSplit}:
  PROOF.sp.bb16 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.bb16)
   # a block of exactly 16 bytes gives them back, masked
   def sp.bb16(ys: List<&2, U32>) -> {Nat.is_eq(B.len(ys), 16n) == True{} : Bool} -> {M.cm.bytes_of(M.cm.block_of(ys)) == B.mask(ys) : List<&2, U32>}:
  PROOF.sp.block_bytes (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.block_bytes)
   # the block of a block's bytes is the block
   def sp.block_bytes(b: M.CmBlock) -> {M.cm.block_of(M.cm.bytes_of(b)) == b : M.CmBlock}:
  PROOF.sp.split_join (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.split_join)
   def sp.split_join(bs: List<&2, M.CmBlock>) -> {M.cm.split(M.cm.join_onto(bs, Nil{})) == M.CmSplit{bs, Nil{}} : M.CmSplit}:
  PROOF.sp.mask_join (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=sp.mask_join)
   def sp.mask_join(bs: List<&2, M.CmBlock>) -> {B.mask(M.cm.join_onto(bs, Nil{})) == M.cm.join_onto(bs, Nil{}) : List<&2, U32>}:
  PROOF.oc.masked (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=oc.masked)
   # Every Octets is masked: to_list(o) = to_list(of_list(to_list(o))) = mask(to_list(o))
   def oc.masked(+o: B.Octets) -> {B.mask(B.Octets.to_list(o)) == B.Octets.to_list(o) : List<&2, U32>}:
  PROOF.oc.len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=oc.len)
   def oc.len(+o: B.Octets, +n: Nat, h: {B.Octets.len(o) == n : Nat}) -> {B.len(B.Octets.to_list(o)) == n : Nat}:
  PROOF.oc.mod (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=oc.mod)
   def oc.mod(+o: B.Octets, h: {Nat.mod(B.Octets.len(o), 16n) == 0n : Nat}) -> {Nat.mod(B.len(B.Octets.to_list(o)), 16n) == 0n : Nat}:
  PROOF.cbcp.iv (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=cbcp.iv)
   # a 16-byte IV is the block of its bytes
   def cbcp.iv(+iv: B.Octets, h: {B.Octets.len(iv) == 16n : Nat}) -> {C.cbc.iv(iv) == Done{M.cm.block_of(B.Octets.to_list(iv))} : Result<&2, &2, M.CmError, M.CmBlock>}:
  PROOF.tr.add_succ (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.add_succ)
   def tr.add_succ(+a: Nat, +n: Nat) -> {Nat.add(a, 1n+n) == 1n+Nat.add(a, n) : Nat}:
  PROOF.tr.add_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.add_zero)
   def tr.add_zero(+a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
  PROOF.tr.rr (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.rr)
   def tr.rr(xs: List<&2, M.CmBlock>, acc: List<&2, M.CmBlock>, b: List<&2, M.CmBlock>) -> {M.cm.blocks.rev_onto(M.cm.blocks.rev_onto(xs, acc), b) == M.cm.blocks.rev_onto(acc, List.append(&2, M.CmBlock, xs, b)) : List<&2, M.CmBlock>}:
  PROOF.tr.append_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.append_eq)
   def tr.append_eq(+xs: List<&2, M.CmBlock>, +ys: List<&2, M.CmBlock>) -> {List.append(&2, M.CmBlock, xs, ys) == M.cm.blocks.append(xs, ys) : List<&2, M.CmBlock>}:
  PROOF.tr.len_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.len_go)
   def tr.len_go(+bs: List<&2, M.CmBlock>, +n: Nat) -> {M.cm.blocks.len.go(bs, n) == Nat.add(List.length(&2, M.CmBlock, bs), n) : Nat}:
  PROOF.tr.len_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.len_eq)
   def tr.len_eq(+bs: List<&2, M.CmBlock>) -> {List.length(&2, M.CmBlock, bs) == M.cm.blocks.len(bs) : Nat}:
  PROOF.tr.split_fin (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.split_fin)
   def tr.split_fin(acc: List<&2, M.CmBlock>, s: M.CmSplit) -> M.CmSplit:
  PROOF.tr.split_fin_cons (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.split_fin_cons)
   def tr.split_fin_cons(+b: M.CmBlock, +acc: List<&2, M.CmBlock>, +s: M.CmSplit) -> {tr.split_fin(Con{b, acc}, s) == tr.split_fin(acc, M.cm.split.cons(b, s)) : M.CmSplit}:
  PROOF.tr.split_fin_nil (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.split_fin_nil)
   def tr.split_fin_nil(+s: M.CmSplit) -> {tr.split_fin(Nil{}, s) == s : M.CmSplit}:
  PROOF.tr.split_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.split_go)
   def tr.split_go(+xs: List<&2, U32>, +acc: List<&2, M.CmBlock>) -> {M.cm.split.go(xs, acc) == tr.split_fin(acc, M.cm.split(xs)) : M.CmSplit}:
  PROOF.tr.split_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.split_eq)
   def tr.split_eq(+xs: List<&2, U32>) -> {M.cm.split(xs) == M.cm.split.fast(xs) : M.CmSplit}:
  PROOF.tr.join_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.join_go)
   def tr.join_go(xs: List<&2, M.CmBlock>, rs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {M.cm.join.go(M.cm.blocks.rev_onto(xs, rs), rest) == M.cm.join.go(rs, M.cm.join_onto(xs, rest)) : List<&2, U32>}:
  PROOF.tr.join_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.join_eq)
   def tr.join_eq(+bs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {M.cm.join_onto(bs, rest) == M.cm.join_onto.fast(bs, rest) : List<&2, U32>}:
  PROOF.tr.cbc_enc_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.cbc_enc_go)
   def tr.cbc_enc_go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +iv: M.CmBlock, +acc: List<&2, M.CmBlock>) -> {C.cbc.enc.go(~K, ~enc, k, bs, iv, acc) == M.cm.blocks.rev_onto(acc, C.cbc.enc(~K, ~enc, k, bs, iv)) : List<&2, M.CmBlock>}:
  PROOF.tr.cbc_enc_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.cbc_enc_eq)
   def tr.cbc_enc_eq(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +bs: List<&2, M.CmBlock>, +iv: M.CmBlock) -> {C.cbc.enc(~K, ~enc, k, bs, iv) == C.cbc.enc.fast(~K, ~enc, k, bs, iv) : List<&2, M.CmBlock>}:
  PROOF.tr.cbc_dec_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.cbc_dec_go)
   def tr.cbc_dec_go(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +iv: M.CmBlock, +acc: List<&2, M.CmBlock>) -> {C.cbc.dec.go(~K, ~dec, k, bs, iv, acc) == M.cm.blocks.rev_onto(acc, C.cbc.dec(~K, ~dec, k, bs, iv)) : List<&2, M.CmBlock>}:
  PROOF.tr.cbc_dec_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.cbc_dec_eq)
   def tr.cbc_dec_eq(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +bs: List<&2, M.CmBlock>, +iv: M.CmBlock) -> {C.cbc.dec(~K, ~dec, k, bs, iv) == C.cbc.dec.fast(~K, ~dec, k, bs, iv) : List<&2, M.CmBlock>}:
  PROOF.tr.xts_enc_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.xts_enc_go)
   def tr.xts_enc_go(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +t: M.CmBlock, +acc: List<&2, M.CmBlock>) -> {T.xts.enc.go(~K, ~enc, k, bs, t, acc) == M.cm.blocks.rev_onto(acc, T.xts.enc(~K, ~enc, k, bs, t)) : List<&2, M.CmBlock>}:
  PROOF.tr.xts_enc_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.xts_enc_eq)
   def tr.xts_enc_eq(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +bs: List<&2, M.CmBlock>, +t: M.CmBlock) -> {T.xts.enc(~K, ~enc, k, bs, t) == T.xts.enc.fast(~K, ~enc, k, bs, t) : List<&2, M.CmBlock>}:
  PROOF.tr.xts_dec_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.xts_dec_go)
   def tr.xts_dec_go(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, bs: List<&2, M.CmBlock>, +t: M.CmBlock, +acc: List<&2, M.CmBlock>) -> {T.xts.dec.go(~K, ~dec, k, bs, t, acc) == M.cm.blocks.rev_onto(acc, T.xts.dec(~K, ~dec, k, bs, t)) : List<&2, M.CmBlock>}:
  PROOF.tr.xts_dec_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.xts_dec_eq)
   def tr.xts_dec_eq(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +bs: List<&2, M.CmBlock>, +t: M.CmBlock) -> {T.xts.dec(~K, ~dec, k, bs, t) == T.xts.dec.fast(~K, ~dec, k, bs, t) : List<&2, M.CmBlock>}:
  PROOF.tr.init_go (https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&name=tr.init_go)
   def tr.init_go(rest: List<&2, M.CmBlock>, +p: M.CmBlock, +acc: List<&2, M.CmBlock>) -> {T.xts.init.go(rest, p, acc) == M.cm.blocks.rev_onto(acc, T.xts.init(rest, p)) : List<&2, M.CmBlock>}:
More: https://jend.leeeet.dev/packages/bend-osdev-cipher-modes.txt?definitions_offset=100