def li.mask_mask

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

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

188def li.mask_mask(zs: List<&2, U32>) -> {B.mask(B.mask(zs)) == B.mask(zs) : List<&2, U32>}:
189  match zs:
190    case Nil{}:
191      {==}
192    case Con{+z, +t}:
193      %bits.byte_byte(z) : {Con{B.byte(B.byte(z)), B.mask(B.mask(t))} == Con{_, B.mask(t)} : List<&2, U32>}
194      %li.mask_mask(t) : {Con{B.byte(B.byte(z)), B.mask(B.mask(t))} == Con{B.byte(B.byte(z)), _} : List<&2, U32>}
195      {==}