def sp.mask_join

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

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

851def sp.mask_join(bs: List<&2, M.CmBlock>) -> {B.mask(M.cm.join_onto(bs, Nil{})) == M.cm.join_onto(bs, Nil{}) : List<&2, U32>}:
852  match bs:
853    case Nil{}:
854      {==}
855    case Con{+b, +t}:
856      %Equal.sym(List<&2, U32>, B.mask(M.cm.bytes_onto(b, M.cm.join_onto(t, Nil{}))), M.cm.bytes_onto(b, B.mask(M.cm.join_onto(t, Nil{}))), sp.mask_blk(b, M.cm.join_onto(t, Nil{}))) : {_ == M.cm.bytes_onto(b, M.cm.join_onto(t, Nil{})) : List<&2, U32>}
857      %Equal.sym(List<&2, U32>, B.mask(M.cm.join_onto(t, Nil{})), M.cm.join_onto(t, Nil{}), sp.mask_join(t)) : {M.cm.bytes_onto(b, _) == M.cm.bytes_onto(b, M.cm.join_onto(t, Nil{})) : List<&2, U32>}
858      {==}