def tr.xts_d1

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

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/xts.bend as T

1160def tr.xts_d1(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, r: Result<&2, &2, M.CmError, M.CmBlock>, +xs: List<&2, U32>) -> {T.xts.d1(~K, ~dec, k, r, xs) == T.xts.d1.fast(~K, ~dec, k, r, xs) : Result<&2, &2, M.CmError, B.Octets>}:
1161  match r:
1162    case Fail{e}:
1163      {==}
1164    case Done{+t}:
1165      %tr.split_eq(xs) : {T.xts.d2(~K, ~dec, k, t, M.cm.split(xs), B.len(xs)) == T.xts.d2.fast(~K, ~dec, k, t, _, B.len.fast(xs)) : Result<&2, &2, M.CmError, B.Octets>}
1166      %BL.len_fast(xs) : {T.xts.d2(~K, ~dec, k, t, M.cm.split(xs), B.len(xs)) == T.xts.d2.fast(~K, ~dec, k, t, M.cm.split(xs), _) : Result<&2, &2, M.CmError, B.Octets>}
1167      tr.xts_d2(~K, ~dec, k, t, M.cm.split(xs), B.len(xs))