def mask_append

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

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

8491def 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>}:
8492  match p:
8493    case Nil{}:
8494      {==}
8495    case Con{+h, +t}:
8496      %mask_append(t, q) : {Con{B.byte(h), B.mask(B.append(t, q))} == Con{B.byte(h), _} : List<&2, U32>}
8497      {==}