def m64_split_joins

bend-osdev-cipher-core@0.1.0.0 · PROOF.bend:200

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
import bend-osdev-cipher-core@0.1.0.0/modes64.bend as X

200def 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>>}:
201  match bs:
202    case Nil{}:
203      {==}
204    case Con{L.LcBlock64{+hi, +lo}, +t}:
205      %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>>}
206      m64_split_joins(t, Con{L.LcBlock64{hi, lo}, acc})