def rx_swap

bend-osdev-gf@0.1.1.0 · PROOF.bend:333

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

333def rx_swap(+a: G.Gf8Bits, +b: G.Gf8Bits, +c: G.Gf8Bits, +d: G.Gf8Bits) -> {G.Gf8Bits.xor(G.Gf8Bits.xor(a, b), G.Gf8Bits.xor(c, d)) == G.Gf8Bits.xor(G.Gf8Bits.xor(a, c), G.Gf8Bits.xor(b, d)) : G.Gf8Bits}:
334  match a b c d:
335    case G.Gf8Bits{+a0, +a1, +a2, +a3, +a4, +a5, +a6, +a7} G.Gf8Bits{+b0, +b1, +b2, +b3, +b4, +b5, +b6, +b7} G.Gf8Bits{+c0, +c1, +c2, +c3, +c4, +c5, +c6, +c7} G.Gf8Bits{+d0, +d1, +d2, +d3, +d4, +d5, +d6, +d7}:
336      rb_eq(Bool.xor(Bool.xor(a0, b0), Bool.xor(c0, d0)), Bool.xor(Bool.xor(a1, b1), Bool.xor(c1, d1)), Bool.xor(Bool.xor(a2, b2), Bool.xor(c2, d2)), Bool.xor(Bool.xor(a3, b3), Bool.xor(c3, d3)), Bool.xor(Bool.xor(a4, b4), Bool.xor(c4, d4)), Bool.xor(Bool.xor(a5, b5), Bool.xor(c5, d5)), Bool.xor(Bool.xor(a6, b6), Bool.xor(c6, d6)), Bool.xor(Bool.xor(a7, b7), Bool.xor(c7, d7)), Bool.xor(Bool.xor(a0, c0), Bool.xor(b0, d0)), Bool.xor(Bool.xor(a1, c1), Bool.xor(b1, d1)), Bool.xor(Bool.xor(a2, c2), Bool.xor(b2, d2)), Bool.xor(Bool.xor(a3, c3), Bool.xor(b3, d3)), Bool.xor(Bool.xor(a4, c4), Bool.xor(b4, d4)), Bool.xor(Bool.xor(a5, c5), Bool.xor(b5, d5)), Bool.xor(Bool.xor(a6, c6), Bool.xor(b6, d6)), Bool.xor(Bool.xor(a7, c7), Bool.xor(b7, d7)), bx_swap(a0, b0, c0, d0), bx_swap(a1, b1, c1, d1), bx_swap(a2, b2, c2, d2), bx_swap(a3, b3, c3, d3), bx_swap(a4, b4, c4, d4), bx_swap(a5, b5, c5, d5), bx_swap(a6, b6, c6, d6), bx_swap(a7, b7, c7, d7))