def word_xx

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

import Base

38def word_xx(n: Nat, a: Word(n), b: Word(n)) -> {a == Word.xor(n, Word.xor(n, a, b), b) : Word(n)}:
39  match n:
40    case 0n:
41      match a b:
42        case WNil{} WNil{}:
43          {==}
44    case 1n+p:
45      match a b:
46        case WCon{ah, at} WCon{bh, bt}:
47          %bool_xx(ah, bh) : {WCon{ah, at} == WCon{_, Word.xor(p, Word.xor(p, at, bt), bt)} : Word(1n+p)}
48          %word_xx(p, at, bt) : {WCon{ah, at} == WCon{ah, _} : Word(1n+p)}
49          {==}