def bx.word

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

import Base

41def bx.word(n: Nat, a: Word(n), b: Word(n)) -> {Word.xor(n, a, Word.xor(n, a, b)) == b : Word(n)}:
42  match n:
43    case 0n:
44      match b:
45        case WNil{}:
46          {==}
47    case 1n+p:
48      match a b:
49        case WCon{ah, at} WCon{bh, bt}:
50          %bx.bool(ah, bh) : {WCon{Bool.xor(ah, Bool.xor(ah, bh)), Word.xor(p, at, Word.xor(p, at, bt))} == WCon{_, bt} : Word(1n+p)}
51          %bx.word(p, at, bt) : {WCon{Bool.xor(ah, Bool.xor(ah, bh)), Word.xor(p, at, Word.xor(p, at, bt))} == WCon{Bool.xor(ah, Bool.xor(ah, bh)), _} : Word(1n+p)}
52          {==}