def bx.rword

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

import Base

1342def bx.rword(n: Nat, a: Word(n), b: Word(n)) -> {Word.xor(n, Word.xor(n, a, b), b) == a : Word(n)}:
1343  match n:
1344    case 0n:
1345      match a:
1346        case WNil{}:
1347          {==}
1348    case 1n+p:
1349      match a b:
1350        case WCon{ah, at} WCon{bh, bt}:
1351          %bx.rbool(ah, bh) : {WCon{Bool.xor(Bool.xor(ah, bh), bh), Word.xor(p, Word.xor(p, at, bt), bt)} == WCon{_, at} : Word(1n+p)}
1352          %bx.rword(p, at, bt) : {WCon{Bool.xor(Bool.xor(ah, bh), bh), Word.xor(p, Word.xor(p, at, bt), bt)} == WCon{Bool.xor(Bool.xor(ah, bh), bh), _} : Word(1n+p)}
1353          {==}