def mask_append

bend-osdev-crypto@0.1.0.0 · PROOF.bend:145

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B

145def mask_append(p: List<&2, U32>, +q: List<&2, U32>) -> {B.mask(B.append(p, q)) == B.append(B.mask(p), B.mask(q)) : List<&2, U32>}:
146  match p:
147    case Nil{}:
148      {==}
149    case Con{+h, +t}:
150      %mask_append(t, q) : {Con{B.byte(h), B.mask(B.append(t, q))} == Con{B.byte(h), _} : List<&2, U32>}
151      {==}