def li.xor_xor

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

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

1645def li.xor_xor(xs: List<&2, U32>, ys: List<&2, U32>) -> {Nat.is_le(B.len(xs), B.len(ys)) == True{} : Bool} -> {M.cm.xor_bytes(M.cm.xor_bytes(xs, ys), ys) == B.mask(xs) : List<&2, U32>}:
1646  match xs:
1647    case Nil{}:
1648      h => {==}
1649    case Con{+a, +s}:
1650      match ys:
1651        case Nil{}:
1652          h => bo.absurd({M.cm.xor_bytes(M.cm.xor_bytes(Con{a, s}, Nil{}), Nil{}) == B.mask(Con{a, s}) : List<&2, U32>}, h)
1653        case Con{+b, +t}:
1654          h => %Equal.sym(U32, B.byte(U32.xor(B.byte(U32.xor(a, b)), b)), B.byte(a), bits.xor_xor(a, b)) : {Con{_, M.cm.xor_bytes(M.cm.xor_bytes(s, t), t)} == Con{B.byte(a), B.mask(s)} : List<&2, U32>}
1655            %Equal.sym(List<&2, U32>, M.cm.xor_bytes(M.cm.xor_bytes(s, t), t), B.mask(s), li.xor_xor(s, t)(h)) : {Con{B.byte(a), _} == Con{B.byte(a), B.mask(s)} : List<&2, U32>}
1656            {==}