def sp.split_join_short

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

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

1420# blocks joined in front of a short tail split back into those blocks and tail
1421def sp.split_join_short(bs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {M.cm.split(rest) == M.CmSplit{Nil{}, rest} : M.CmSplit} -> {M.cm.split(M.cm.join_onto(bs, rest)) == M.CmSplit{bs, rest} : M.CmSplit}:
1422  match bs:
1423    case Nil{}:
1424      h => h
1425    case Con{+b, +t}:
1426      h => %Equal.sym(M.CmSplit, M.cm.split(M.cm.bytes_onto(b, M.cm.join_onto(t, rest))), M.cm.split.cons(b, M.cm.split(M.cm.join_onto(t, rest))), sp.blk(b, M.cm.join_onto(t, rest))) : {_ == M.CmSplit{Con{b, t}, rest} : M.CmSplit}
1427        %Equal.sym(M.CmSplit, M.cm.split(M.cm.join_onto(t, rest)), M.CmSplit{t, rest}, sp.split_join_short(t, rest)(h)) : {M.cm.split.cons(b, _) == M.CmSplit{Con{b, t}, rest} : M.CmSplit}
1428        {==}