def xor_bits

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/xbits.bend:174

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L

174# swap ^= k_t on bits
175def xor_bits(+a: U32, +b: U32, +na: Nat, +nb: Nat, +ea: {v(a) == na : Nat}, +eb: {v(b) == nb : Nat}, +ha: {Nat.is_le(na, 1n) == True{} : Bool}, +hb: {Nat.is_le(nb, 1n) == True{} : Bool}) -> {v(U32.xor(a, b)) == S.bxor(na, nb) : Nat}:
176  match na nb:
177    case 0n 0n:
178      %Equal.sym(U32, a, 0, u0(a, ea)) : {v(U32.xor(_, b)) == 0n : Nat}
179      %Equal.sym(U32, b, 0, u0(b, eb)) : {v(U32.xor(0, _)) == 0n : Nat}
180      {==}
181    case 0n 1n:
182      %Equal.sym(U32, a, 0, u0(a, ea)) : {v(U32.xor(_, b)) == 1n : Nat}
183      %Equal.sym(U32, b, 1, u1(b, eb)) : {v(U32.xor(0, _)) == 1n : Nat}
184      {==}
185    case 1n 0n:
186      %Equal.sym(U32, a, 1, u1(a, ea)) : {v(U32.xor(_, b)) == 1n : Nat}
187      %Equal.sym(U32, b, 0, u0(b, eb)) : {v(U32.xor(1, _)) == 1n : Nat}
188      {==}
189    case 1n 1n:
190      %Equal.sym(U32, a, 1, u1(a, ea)) : {v(U32.xor(_, b)) == 0n : Nat}
191      %Equal.sym(U32, b, 1, u1(b, eb)) : {v(U32.xor(1, _)) == 0n : Nat}
192      {==}
193    case 2n+q _:
194      Empty.absurd({v(U32.xor(a, b)) == S.bxor(2n+q, nb) : Nat}, L.false_true(ha))
195    case _ 2n+q:
196      Empty.absurd({v(U32.xor(a, b)) == S.bxor(na, 2n+q) : Nat}, L.false_true(hb))