def tr.xts_e2

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

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
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

1129def tr.xts_e2(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, +k: K, +t: M.CmBlock, s: M.CmSplit, +n: Nat) -> {T.xts.e2(~K, ~enc, k, t, s, n) == T.xts.e2.fast(~K, ~enc, k, t, s, n) : Result<&2, &2, M.CmError, B.Octets>}:
1130  match s:
1131    case M.CmSplit{bs, +tail}:
1132      match bs:
1133        case Nil{}:
1134          {==}
1135        case Con{+p, +rest}:
1136          %tr.init_eq(rest, p) : {Done{B.Octets.of_list(T.xts.eout(~K, ~enc, k, t, T.xts.init(rest, p), T.xts.last(rest, p), tail))} == Done{B.Octets.of_list(T.xts.eout.fast(~K, ~enc, k, t, _, T.xts.last(rest, p), tail))} : Result<&2, &2, M.CmError, B.Octets>}
1137          %tr.xts_eout(~K, ~enc, k, t, T.xts.init(rest, p), T.xts.last(rest, p), tail) : {Done{B.Octets.of_list(T.xts.eout(~K, ~enc, k, t, T.xts.init(rest, p), T.xts.last(rest, p), tail))} == Done{B.Octets.of_list(_)} : Result<&2, &2, M.CmError, B.Octets>}
1138          {==}