def li.mask_xor

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

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

1620def li.mask_xor(xs: List<&2, U32>, ys: List<&2, U32>) -> {B.mask(M.cm.xor_bytes(xs, ys)) == M.cm.xor_bytes(xs, ys) : List<&2, U32>}:
1621  match xs:
1622    case Nil{}:
1623      {==}
1624    case Con{+a, +s}:
1625      match ys:
1626        case Nil{}:
1627          {==}
1628        case Con{+b, +t}:
1629          %bits.byte_byte(U32.xor(a, b)) : {Con{B.byte(B.byte(U32.xor(a, b))), B.mask(M.cm.xor_bytes(s, t))} == Con{_, M.cm.xor_bytes(s, t)} : List<&2, U32>}
1630          %li.mask_xor(s, t) : {Con{B.byte(B.byte(U32.xor(a, b))), B.mask(M.cm.xor_bytes(s, t))} == Con{B.byte(B.byte(U32.xor(a, b))), _} : List<&2, U32>}
1631          {==}