def tr.xts_d2

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

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

1140def tr.xts_d2(~K: Data, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, +t: M.CmBlock, s: M.CmSplit, +n: Nat) -> {T.xts.d2(~K, ~dec, k, t, s, n) == T.xts.d2.fast(~K, ~dec, k, t, s, n) : Result<&2, &2, M.CmError, B.Octets>}:
1141  match s:
1142    case M.CmSplit{bs, +tail}:
1143      match bs:
1144        case Nil{}:
1145          {==}
1146        case Con{+c, +rest}:
1147          %tr.init_eq(rest, c) : {Done{B.Octets.of_list(T.xts.dout(~K, ~dec, k, t, T.xts.init(rest, c), T.xts.last(rest, c), tail))} == Done{B.Octets.of_list(T.xts.dout.fast(~K, ~dec, k, t, _, T.xts.last(rest, c), tail))} : Result<&2, &2, M.CmError, B.Octets>}
1148          %tr.xts_dout(~K, ~dec, k, t, T.xts.init(rest, c), T.xts.last(rest, c), tail) : {Done{B.Octets.of_list(T.xts.dout(~K, ~dec, k, t, T.xts.init(rest, c), T.xts.last(rest, c), tail))} == Done{B.Octets.of_list(_)} : Result<&2, &2, M.CmError, B.Octets>}
1149          {==}