def m64_split_joins

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:8546

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
import bend-osdev-legacy-ciphers@0.1.0.0/modes64.bend as X

8546def m64_split_joins(bs: List<&2, L.LcBlock64>, +acc: List<&2, L.LcBlock64>) -> {X.m64.split(B.mask(m64_joins(bs, Nil{})), acc) == Some{X.m64.rev_onto(acc, bs)} : Maybe<&2, List<&2, L.LcBlock64>>}:
8547  match bs:
8548    case Nil{}:
8549      {==}
8550    case Con{L.LcBlock64{+hi, +lo}, +t}:
8551      %blk8(hi, lo) : {X.m64.split(B.mask(m64_joins(t, Nil{})), Con{_, acc}) == Some{X.m64.rev_onto(acc, Con{L.LcBlock64{hi, lo}, t})} : Maybe<&2, List<&2, L.LcBlock64>>}
8552      m64_split_joins(t, Con{L.LcBlock64{hi, lo}, acc})